University of Pernambuco, Recife (BRAZIL)
CADP (Construction and Analysis of Distributed Processes)
about 1200 lines of LOTOS
Due to their inherent complexity, specifications of middleware systems
are not trivial to understand. In particular, middleware systems have
not only to hide the complexity and hazards of the communication
network, but also to offer an increasing number of services, the
properties of which are often described only informally.
To study the suitability of using formal specification and verification techniques, a formal model of CORBA in LOTOS has been developed. Using CADP, it was possible to simulate the LOTOS model and to verify behavioral properties, such as absence of deadlocks, livelocks, or the presence of particular execution sequences. Furthermore, using equivalence checking, it was possible to compare different middleware service compositions.
This study demonstrated that the use of LOTOS and CADP allows to check
behavioral properties of middleware systems.
The work also opens new research directions, such as the use of the Petri Nets generated by the CAESAR compiler of CADP for the performance and reliability analysis of middleware specifications.
Nelson Souto Rosa and Paulo Roberto Freire Cunha.
"A Software Architecture-Based Approach for Formalising Middleware
Behaviour". In Proceedings of the Workshop on Formal Foundation of
Embedded Software and Component-based Software Architectures FESCA2004
(Barcelona, Spain), Electronic Notes in Theoretical Computer
Science, vol. 108, pp. 39-51, December 2004.
Available on-line from http://www.csse.monash.edu.au/fesca/Pdf-Files/3-rosa.pdf
or from the CADP Web site in PDF or PostScript
Nelson Souto Rosa
Centro de Informatica
Universidade Federal de Pernambuco
50732-970 Recife, Pernambuco
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|