Database of Research Tools Developed Using CADP

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


Last modified: Thu Feb 11 12:23:11 2021.


Back to the CADP research tools page