Database of Case Studies Achieved Using CADP

Bus Instrumentation Protocol

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.
Pierre Azema
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:

Last modified: Fri Jul 18 16:30:34 2014.

Back to the CADP case studies page