Equipment Failure Management Protocol

Organisation:	INRIA Grenoble Rhône-Alpes (FRANCE)
Method:	SAM, LNT, temporal logic
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Embedded Systems for Avionics.
Period:	2009
Size:	4,000 lines of LNT
Description:	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 by AIRBUS. 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.
Contact:	INRIA/VASY project-team 655, avenue de l'Europe Montbonnot 38334 St Ismier Cedex FRANCE Fax: +33 476 61 52 00 Email: cadp@inria.fr
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