Database of Case Studies Achieved Using CADP

Formalising Middleware Behaviour using LOTOS.

Organisation: University of Pernambuco, Recife (BRAZIL)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Middleware.

Period: 2004

Size: about 1200 lines of LOTOS

Description: 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.

Conclusions: 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.

Publications: [Rosa-Cunha-04] 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 our FTP site in PDF or PostScript
Contact:
Nelson Souto Rosa
Centro de Informatica
Universidade Federal de Pernambuco
50732-970 Recife, Pernambuco
BRAZIL



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page