Ahlem Triki, Borzoo Bonakdarpoor, Jacques Combaz
Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models (2015)
Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models (2015)
TR-2015-2.pdf
Keywords: Concurrent Real-Time Systems, BIP, Correct-by-construction
Abstract: Correct implementation of concurrent real-time systems has always been a tedious task due to their inherent complex structure; concurrency introduces a great deal of non-determinism, which can potentially conflict with meeting timing constraints. In this paper, we focus on model-based concurrent implementation of timed models. Our abstract models consist of a set of components interacting with each other using multi-party interactions. Each component is internally subject to a set of timing constraints. We propose a chain of transformations that starts with an abstract model as input and generates correct-by-construction executable code as output. We show that all transformed models are observationally equivalent to the abstract model through bisimulation proofs and, hence, all functional properties of the abstract model are preserved. To facilitate developing the proofs of correctness, each transformation obtains a model by incorporating a subset of physical constraints (e.g., type of communication and global clock synchronization). Our method is fully implemented and validated on a real-time multi-sensor image reconstruction system outperforms the corresponding concurrent implementation managed by a centralized scheduler.
