Information Technology Reference
In-Depth Information
method with correct flow of control (i.e., the conditional choice and loop state-
ments). Furthermore, the model of the detailed design specifies class invariants
and the functionalities of each class method in terms of its precondition and
postcondition. This makes it possible for these conditions to be automatically in-
serted as assertions into the code generated. Therefore, code will have method
bodies with method invocations and assertions .Wecallsuchacodea probably
correct code . Static analysis techniques and tools such as ESCJava [11] can be
used for verification of correctness of the code against the design model.
The Construction Programmer can now work on the generated code with
method invocations and assertions, and produce executable code. However, the
assertions should not be removed and thus the result should be code with as-
sertions. Testing and static analysis again can be carried out with the aid of
tools such as ESCJava and JML. If the assertions are written in Spec# asser-
tion commands and the Construction Programmer code the program in Spec#,
the executable code could be a Spec# program. In this case, the Spec# compiler
takes care of the static analysis. We think it would be significant for Spec# to
be realistically useful as it is not feasible for a programmer to code the assertion
commands correctly. The assertions should be derived from the design models.
An important advantage of our proposed method would be that these assertions
would be already included in the code generated by the Construction Manager
from the model, and the Construction Programmer would be bound to follow and
aim to assure these assertions.
5Conluon
We have presented our experience in the application of a formal calculus to the
CoCoME case study.
Our experience shows the need of a semantic model that formalises the main
concepts and software entities in a model-driven development, and supports multi-
view modelling and separation of concerns in a complex software development.
rCOS provides these formalisations and support. Model-driven development must
also complemented with property-driven analysis techniques. Properties are spec-
ified in rCOS as logical formulas and algebraic properties of modelling elements
that are formulated as mathematical structures. The algebraic properties form
the foundation for model transformations. To ensure consistency and correctness,
both static and dynamic consistency of the specification must be checked, and
both abstraction and refinement techniques are needed for model transformation
and analysis. The work also shows that different models and tools are more effec-
tive on the design and analysis of some aspects than the others. Proved correct
model transformations should be carried out side by side with verification and
validation. Correct model transformations preserve properties, so that it is not
required to verify again, and verification and validation are used to check the con-
dition on when the transformations can be applied and extra properties required
for the transformed model. rCOS is a methodology that supports a consistent use
of different techniques and tools for modelling, design, verification and validation.
 
Search WWH ::




Custom Search