Graz University of Technology (AUSTRIA)
CADP (Construction and Analysis of Distributed Processes)
The design process of complex systems by using software
architectures usually consists in deriving a first architectural
model of the system from the initial requirements, and then to
refine the model until an appropriate level of detail is reached.
This may result in a completely restructured model, which may not
satisfy a formal refinement relation with the predecessor model.
Formal methods are helpful in formalizing and argumenting about
the preservation of desired properties when refining architectural
descriptions. This case-study illustrates and analyses architectural
refinement by using LOTOS as architectural description language and
the model-checking capabilities of the CADP toolbox.
The architecture considered consists of three components P, P, Q, which are chained together according to a call-return architectural pattern. Each component performs some computation, calls its neighbour via channel c and waits for the result from its neighbour via channel r. Component Q (the last of the chain) completes the computation and sends back the result, which is forwarded back through the chain without modification. A drawback of this pattern is that all components P are locked until the computation has passed down the chain and returned a result. To increase efficiency by allowing a component P to be ready for the next computation right after the call down the chain, the system is changed to a batch-sequential architectural pattern in which the result is delivered by the last component Q without passing back through the chain. The two versions of the architecture were specified in LOTOS.
The two architectural patterns are not related by any classical refinement relation, since the property "it is not possible to start a new computation before the previous one has finished" does not hold anymore in the batch-sequential pattern. Other properties continue to hold, e.g., the fact that each call is eventually followed by a result, or that messages returned from Q are eventually forwarded without change. These properties were expressed as ACTL formulas and verified on the LTSs of the two LOTOS specifications using the XTL model-checker of CADP.
When transforming the architecture of a system during the design
process (e.g., to achieve an increase in efficiency), some
requirements may not be preserved anymore. In such cases, the new
system is not related to the previous one by a formal refinement
relation, and still it describes the desired architecture. Analysis
by model-checking is useful in order to establish which properties
are preserved, and what are the new interesting properties of the
[Kerschbaumer-02] Andreas Kerschbaumer.
"Non-refinement Transformations of Software Architectures". In
Michael Butler and Traian Muntean, editors, Proceedings of the
International Workshop on Refinement of Critical Systems: Methods,
Tools and Experience RCS'02 (Grenoble, France), January 2002.
Available on-line at: ftp://ftp.ist.tu-graz.ac.at/pub/publications/IST-TEC-02-01.pdf
or from the CADP Web site in PDF or PostScript
Dipl.-Ing. Dr. Andreas Kerschbaumer
Logim Software GmbH
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies