Designing Safe Synchronous Reactive Systems

Organisation:	University M'hamed Bougara / LIMOSE, Boumerdes, ALGERIA Télécom ParisTech / LTCI, FRANCE
Method:	I/O-automata
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Embedded Systems.
Period:	2019
Size:	n/a
Description:	An approach to manage the growing complexity of embedded systems is the component-based design. In addition to this complexity, one has to manage also the strict reliability and correctness constraints required for these systems. This work proposes a theoretical framework for developing correct reactive synchronous components (SR-components) compositionally. The SR-components considered are characterized by their memory (M) and their latency (L) between an action and the corresponding reaction. SR-components are modeled as I/O-automata, which are suitable for modeling reactive components and also enable hierarchical construction of systems by a composition operator. Since the composition operator of I/O-automata does not preserve the semantics of SR-components connected in a pipeline (i.e., the resulting I/O-automaton does not have the characteristics of an SR-pipeline), a new I/O-automata constraint-based composition operator is proposed and shown to preserve the semantics of pipeline composition of SR-components. The constraint-based composition operator was validated on several examples by checking the bisimilarity between the pipeline composition of SR-components and the expected global SR-pipeline using CADP. Also, the framework was experimented on a real-life case-study, namely an IDCT (Inverse Discrete Cosine Transform) signal processing application, which consists of seven SR-components connected serially and communicating by rendezvous. The generated SR-models were used to verify data-based temporal logic properties expressed in MCL.
Conclusions:	The proposed framework makes possible the modeling of synchronous reactive systems and their composition, and enables to reason about complex serial compositions of synchronous components. The models are based on I/O-automata, which are able to model various kinds of components (physical, software, communication channels, sensors, etc.) and are therefore beneficial for the engineering of complex systems. The proposed model construction algorithms were implemented and verified using the CADP tools. The new constraint-based composition operator for I/O-automata avoids the state space explosion problem for complex compositions.
Publications:	[Chabane-AmeurBoulifa-Mohamed-19] Sarah Chabane, Rabéa Ameur-Boulifa, and Mezghiche Mohamed. "Vers une conception de systèmes réactifs synchrones sûrs". Actes du 12ème Colloque sur la Modélisation des Systèmes Réactifs MSR'2019 (Angers, France), Nov. 2019. Available on-line at: http://msr2019.laris.univ-angers.fr/pdf/MSR19_paper_3.pdf or from the CADP Web site in PDF or PostScript [Chabane-AmeurBoulifa-Mohamed-21] Sarah Chabane, Rabéa Ameur-Boulifa, and Mezghiche Mohamed. "Towards Compositional Verification of Synchronous Reactive Systems". International Journal of Critical Computer-Based Systems 10(2):120-142, September 2021. Available on-line at: https://www.inderscienceonline.com/doi/abs/10.1504/IJCCBS.2021.117995
Contact:	Rabéa Ameur-Boulifa Laboratoire System-On-Chip, TELECOM ParisTech Institut EURECOM Les Templiers, 450, route des Chappes, F-06410 Biot FRANCE Tel: +33 (0)4 93 00 84 01 Email: Rabea.Ameur-Boulifa@telecom-paristech.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