|
| 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: |
LAAS (Laboratoire d'Automatique et d'Analyse des Systemes) Toulouse,
France
|
|---|---|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Real-time process control.
|
| Period: |
1990
|
| Size: |
215 lines of LOTOS.
|
| Description: |
Several devices, sensors or actuators are interconnected by a Bus.
The Bus Instrumentation protocol deals with the updating of distributed
buffers by means of broadcast operations. This protocol is implemented
at the data link layer (OSI layer 2).
From requirements expressed in natural language, several constraints on execution sequences (or temporal logic assertions) are derived. Specific LOTOS techniques, namely observational equivalent behaviours, have been used to check if the proposed protocol meets these requirements. A careful analysis of the behaviour has been performed with respect to user requirements. |
| Conclusions: |
In this study, we experimented with the fast definition of user
expectations with respect to the relative ordering of visible
primitives. In this process, either the specification has to be
revised or the requirement itself has to be modified, both cases result
in a better characterization of the facility offered by the service.
|
| Publications: |
Pierre Azema, Khalil Drira, and François Vernadat.
A bus instrumentation protocol specified in LOTOS. In Juan Quemada,
Jose Manas, and Enrique Vazquez, editors, Proceedings of the 3rd
International Conference on Formal Description Techniques FORTE'90
(Madrid, Spain), November 1990.
Available on-line from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Pierre Azema LAAS-CNRS 7 Avenue Colonel Roche F-31077 Toulouse cedex FRANCE tel: +33 5 61 33 63 63 fax: +33 5 61 33 64 11 E-mail: [email protected] |
| 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