University M'hamed Bougara / LIMOSE, Boumerdes, ALGERIA
Télécom ParisTech / LTCI, FRANCE
CADP (Construction and Analysis of Distributed Processes)
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)
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.
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
Sarah Chabane, Rabéa Ameur-Boulifa, and Mezghiche Mohamed.
"Vers une conception de systèmes réactifs synchrones
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
Laboratoire System-On-Chip, TELECOM ParisTech
Les Templiers, 450, route des Chappes, F-06410 Biot
Tel: +33 (0)4 93 00 84 01
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|