Non-Refinement Transformations of Software Architectures.

Organisation:	Graz University of Technology (AUSTRIA)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Software Architectures.
Period:	2001-2002
Size:	n/a
Description:	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.
Conclusions:	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 transformed architecture.
Publications:	[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
Contact:	Dipl.-Ing. Dr. Andreas Kerschbaumer Software Architect Logim Software GmbH Neuschloss 1 8142 Wundschuh AUSTRIA E-mail: kerschbaumer@ist.tugraz.at
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page