Formal Analysis of Distributed Reactive Applications

Organisation:	Université M'hamed Bougara, Boumerdes (ALGERIA) Télécom ParisTech, Université Paris-Saclay (FRANCE)
Functionality:	Formal Analysis of Distributed Reactive Applications
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2017
Description:	Compositional verification techniques are a useful approach to cope with the limitations of formal verification of complex component-based systems. However, as they are generally applied on abstract models rather than the concrete system components, the analysis and prediction of inter-dependencies of the overall system is still challenging. Therefore the authors promote a correct-by-construction approach, providing design rules to build correct systems from correct components. Components of a distributed reactive application are modeled as I/O automata, akin to synchronous dataflow models called SR-models. Each component has its own set of parameters (latency and memory). Composition rules ensure composability and guarantee correct composition of SR-models. The proposed framework comprises two main activities. First, the construction of the model. To increase the reusability, a library of previously designed and verified components helps in the construction. Second, the verification of the global model relies on the automatic analysis enabled by model-checking with CADP. The proposed framework is illustrated on an Inverse Discret Cosine Transform.
Conclusions:	The CADP toolbox "offers a wide range of functionalities among which model checking and equivalence checking".
Publications:	[Chabane-AmeurBoulifa-Mezghiche-17-a] Sarah Chabane, Rabéa Ameur-Boulifa, and Mohamed Mezghiche. "Rethinking of I/O-automata composition". Proceedings of the Forum on Specification and Design Languages (FDL 2017), Verona, Italy, IEEE, September 2017. Available on-line at: http://doi.org/10.1109/FDL.2017.8303892 or from the CADP Web site in PDF or PostScript [Chabane-AmeurBoulifa-Mezghiche-17-b] Sarah Chabane, Rabéa Ameur-Boulifa, and Mohamed Mezghiche. "Formal Framework for Automated Analysis and Verification of Distributed Reactive Applications". Proceedings of the 1st International Conference on Embedded & Distributed Systems (EDiS), Oran, Algeria, IEEE, December 2017. Available on-line at: https://doi.org/10.1109/EDIS.2017.8284026 or from the CADP Web site in PDF or PostScript
Contact:	Rabéa Ameur-Boulifa Eurecom - Télécom ParisTech 450, route des Chappes 06410 Biot FRANCE Email: Rabea.Ameur-Boulifa at telecom-paristech.fr Tel: +33 (0)4 93 00 84 01 Fax: +33 (0)4 93 00 82 00
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page