LAAS (Laboratoire d'Automatique et d'Analyse des Systemes) Toulouse,
CADP (Construction and Analysis of Distributed Processes)
Real-time process control.
215 lines of LOTOS.
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.
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.
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 our FTP site in PDF or PostScript
7 Avenue Colonel Roche
F-31077 Toulouse cedex
tel: +33 5 61 33 63 63
fax: +33 5 61 33 64 11
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|