|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 the CADP Web 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 |
Back to the CADP case studies page