INRIA Grenoble Rhône-Alpes (FRANCE)
SAM, LNT, temporal logic
CADP (Construction and Analysis of Distributed Processes)
Embedded Systems for Avionics.
4,000 lines of LNT
This study was done in the framework of the TOPCASED project. The
object of the study was a proprietary protocol, which aims at managing
equipment failures on airplanes. This protocol was specified as two
automata described in SAM, a graphical synchronous language developed
A methodology developed for a previous avionics case-study was applied to this example: The two SAM automata modelling the protocol were translated into a set of LNT types and functions with boolean inputs/outputs (about 2,000 lines of LNT code). This step was made fully automatic by developing an ACCELEO plugin that implements this translation within ECLIPSE.
Additional LNT code (about 2,000 lines) was written manually to model: (1) the two "wrapper" processes encapsulating the LNT functions generated from the SAM automata; (2) extra protocol functionality not specified in the original SAM automaton; (3) bounded FIFO queues connecting the different parts of the system; and (4) the expected behaviour of the system's environment.
Then, the LNT specification was analyzed using the CADP tools: step-by-step simulation, generation of state spaces (about 100,000 states for a FIFO of length 3), equivalence checking and model checking of various properties expressed in temporal logic regarding, e.g., the activation/expiration of timers and the correct restransmission of requests on timeouts. This analysis enabled the detection of errors in the SAM specification. After correction of these errors, the protocol specification was proven equivalent to a model of the expected service.
A SAM automaton in a TOPCASED editor
|Conclusions:||This case-study constitutes an example of a simple and elegant approach, in which CADP plays a central role, for modelling and analysing GALS (Globally Asynchronous, Locally Synchronous) systems in the hardware design community.|
655, avenue de l'Europe
38334 St Ismier Cedex
Fax: +33 476 61 52 00
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|