Verification and Life Cycle Management
You and your colleagues are most likely familiar with systems development life cycle management and some, or possibly many, software assurance practices. Not all life cycles are suitable for our purpose. Most lack even a vocabulary to describe verification. Further, the activities and tasks don’t describe type safety. Early verification means our life cycle needs to say more than Test. In most cases Test happens just before go-live, or maybe after. Ouch ! Even worse, few life cycles have a recurring structure that avoids the well-known waterfall blunder.
More good news. The Software and Systems Process Engineering Metamodel [SPEM 2008] is a standard that allows us to define the activities and tasks that describe type safety. Specialization of the “meta model” defines the vocabulary. It allows a recurring structure and is sufficiently general to be tailored to all known software methods.
In addition to the recurring structure SPEM avoids the waterfall blunder by splitting the vocabulary that describes activities from the vocabulary that describes phases. We call these activities disciplines. It’s a neat trick originally part of the Unified Process. Figure 1, the Hump Chart, illustrates the general approach.
Figure 1. The Hump Chart.
Disciplines are represented on the vertical axis. Reading from Business Modeling at the top left down to Deployment, disciplines are “a categorization of activities based on similarity of concerns and cooperation of work effort.” Many life cycles incorrectly use a similar vocabulary to describe phases. Phases, represented on the horizontal axis, beginning on the left with Inception and ending at the far right with Transition, represent the time ordered sequence of events. Notice the unusual vocabulary of phases. The vocabulary of the phases describes the time ordered sequence of events rather than activities. Splitting the vocabularies removes a sequential dependency that caused Winston Royce to warn against Waterfall [R 1970]. Phases contain iterations. Iterations, just below the phases are labeled with the first letter of each phase followed by an integer. Within each iteration, a hump represents the level of effort for that discipline. Also notice the hump for Test in the Elaboration, Construction and Transition phases.
We specialize the general approach with an Early Evolutionary life cycle [GAS 2005] tailored to verification. Figure 2 illustrates an implementation of the life cycle as a Method Plugin using the Eclipse Process Framework. The left pane labeled Library shows that the Type Safe Method Plugin defines four life cycles: Early Evolutionary, Grand Design, Incremental Construction and Waterfall. SPEM provides the semantics of the containment hierarchy above the life cycles. In short, Process and Capability Pattern are elements of the Method Architecture. Life cycles are reusable capability patterns. We choose the Early Evolutionary life cycle because it provides more than one iteration in the early phases – inception, elaboration and construction where type safety provides verification. The Software Assurance Configuration is the default configuration for the Type Safe Method plug-in.
Figure 2. A Method Plug-in with Early Evolutionary Life Cycle as Capability Pattern.
Also in Figure 2, the right pane shows a work break down structure with phases and named iterations. As with the names of phases, iteration names must meaningfully describe the time ordered sequence of events, rather than disciplines. The Elaboration phase contains Amplification and Synthesis iterations. In the Amplification iteration the type safe technical architecture framework is reviewed with the development team and work begins on forward engineering an application specific architecture from the framework. Further, parametric types, casts, option types and type safe operations are reviewed with development team. In the Synthesis iteration parametric class diagrams and sequence diagrams annotated with type parameters are specified. Next, the type safe application specific architecture is forward engineered. The model is also checked against running code. The Elaboration phase ends with the Executable Architecture milestone where the application specific model derived from architecture framework is verified for type safety. Demonstrations are conducted for the development team and round trip engineering gains focus over forward engineering.
The Construction phase contains Type Specification, Test Execution and Run-time Verification iterations. In the Type Specification iteration, generic types are analyzed and specified for use by the developer to ensure compile-time constraints are enforced. “Stupid” and incorrect down casts are avoided and type enforcement conventions used in static analysis are incorporated. During Test Execution parametric class types pass compile-time checks. Tests in all test cases validate casts in source code as it is developed and functions and operations satisfy run-time constraints. Option type conventions are validated against static analysis rules. In Run-time Verification, the development team execute continuous integration and regression test. Run-time types and values are verified throughout and verification of source against static analysis rules. Construction ends with the Verified Release milestone. In Verified Release verification through type safety is complete. Raw types have been converted to generic types. Casts are verified through unit test with zero defects. All encoded Option types pass static analysis checks.
Concluding our tour of the right pane, the column labeled type lists whether the row entry is a capability pattern, phase, iteration, or milestone. The columns labeled planned and repeat allow the process engineer to select a check box indicating that planned and repeatable are true for that row and column entry. We assume the inception phase is exclusively functional ending in defined objectives. We do not discuss the inception phase further. Deployment occurs in the transition phase which we do not discuss. Table 1 summaries iteration names.
Table 1 – Named iterations in the Early Evolutionary life cycle.
| Term | Definition |
|---|---|
| Amplification Iteration | Type safe technical architecture framework is reviewed with development team and work begins on forward engineering application specific architecture from framework. Parametric types, casts, option types and type safe operations are reviewed with development team. |
| Synthesis Iteration | Parametric Class diagrams and Sequence diagrams annotated with type parameters are specified. Type safe application specific architecture is forward engineered. Model is checked against running code. |
| Executable Architecture Milestone | Application specific model derived from architecture framework is verified for type safety. Demonstrations are conducted for development team. Round trip engineering gains focus over forward engineering. |
| Type Specification Iteration | Generic types are analyzed and specified for use by the developer to ensure compile-time constraints are enforced. “Stupid” and incorrect down casts are avoided. Type enforcement conventions used in static analysis are incorporated. |
| Test Execution Iteration | Parametric class types pass compile-time checks. Tests in all test cases validate casts in source code as it is developed. Functions and operations satisfy run-time constraints. Option type conventions are validated against static analysis rules. |
| Run-time Verification Iteration | Execute continuous integration and regression. Run-time types and values are verified throughout. Verification of source against static analysis rules. Repeat. |
| Verified Release Milestone | Verification through type safety is complete. Raw types are converted to generic types. Casts are verified through unit test with zero defects. All encoded Option types pass static analysis checks. Deployment to production. |
Disciplines describe the activities of type safe verification. The activities of Type Safe Design require an architect or engineer to analyze types to enforce compile-time constraints. Specify parametric types and convert raw types to parametric types. Refactor “stupid” and incorrect down casts into allowable casts. Execute static type checks and type inference on incomplete implementation. The Interactive Proving discipline implies that an architect elaborate operations and functions to satisfy type safe constraints with the help of type checking and type inference tools. And the Test Driven Development discipline requires a developer to develop compile-time and run-time tests and specify expected results. Specify and execute tests and develop source code concurrently testing allowable casts. Encode source with Option types according to conventions to be tested against static analysis rules.With the Early Evolutionary life cycle specified we now define disciplines. Again in the left pane of Figure 3, under Library, we have expanded Method Content where we see three disciplines: Type Safe Design, Interactive Proving and Test Driven Development. SPEM also provides the semantics of the containment hierarchy for disciplines. In short, Standard Categories and Disciplines are elements of the Method Content.
Figure 3. Disciplines as Standard Categories. Discipline specialized as Type Safe Design, InteractiveProving and Test Driven Development.
The fields in the right pane of the Type Safe Design, Interactive Proving and Test Driven Development tabs allow elaboration with brief and main descriptions as would fields in the Task, Reference Workflow, and Guidance tabs. Further elaboration includes Domain, Work Product Kind, Role Set and Tool as standard categories. Notice that we have not defined roles though we referenced them in the definition of disciplines. Scope limitations preclude a full elaboration of roles and various fields refining disciplines at this time.
Table 2 – Type Safe Disciplines
| Term | Definition |
|---|---|
| Type Safe Design Discipline | Analyze types to enforce compile-time constraints. Specify parametric types and convert raw types to parametric types. Refactor “stupid” and incorrect down casts into allowable casts. Execute static type checks and type inference on incomplete implementation. |
| Interactive Proving Discipline | Elaborate operations and functions to satisfy type safe constraints with the help of type checking and type inference tools. |
| Test Driven Development Discipline | Develop compile-time and run-time tests and specify expected results. Specify and execute tests and develop source code concurrently testing allowable casts. Encode source with Option types according to conventions to be tested against static analysis rules. |
Our life cycle is now defined. We understand what it means to say early verification. In contrast to a large commitment to Test at the end of the life cycle, the Type Safe Design, Interacting Proving and Test Driven Development disciplines are allocated some level of effort during the both the Elaboration and Construction phases. Individuals familiar with Test Driven Development will recognize the importance of the approach. An updated hump chart would visualize the relative level of effort for each discipline within each iteration. We understand the Amplification, Synthesis, Type Specification and Test Execution iterations because they are defined rather than just indeterminate numbered re-recurrences. The next section called Early Verification with Type Safe Technical Architecture explains how artifacts created during the Elaboration Phase represent type safety. The section following called Type Safety and Software Verification provides artifacts from the Construction Phase.