Implementabilty and Robustness of Timed Systems – ImpRo
Implementability and Robustness of Timed Systems
Towards models closer to their implementation
The project ImpRo, «Implementability and Robustness of Timed Systems« addresses<br />the issues related to the practical implementation of formal models for the<br />design of communicating embedded systems: such models abstract many complex<br />features or limitations of the execution environment. The modeling of time, in<br />particular, is usually ideal, with infinitely precise clocks, instantaneous<br />tests or mode commutations, etc.<br /><br />Our objective is thus to study to what extent the practical implementation of<br />these models preserves their good properties.
We will first define a generic
mathematical framework to reason about and measure implementability, and then
study the possibility to integrate implementability constraints in the models.
We will particularly focus on the combination of several sources of
perturbation such as resource allocation, the distributed architecture of
applications, etc. We will also study implementability through control and
diagnostic techniques. We will finally apply the developed methods to a case
study based on the AUTOSAR architecture, a standard of the automotive industry
The project is not finished yet
The project is not finished yet
Up to the 1/07/2012, about 10 publications in acknowledged international journals and conferences.
The aim of this proposal is the study of the relation between models for
embedded systems design and their practical implementation: such models indeed
abstract many complex details or restrictions of the execution environment.
We focus on well-known mathematically defined models, such as timed automata or
time Petri nets. Such models can be derived from higher-level formalisms such
as UML or AADL, but this will be deliberately out of the scope of our study.
With those formal timed models, the distance between the model and its
implementation may be particularly important: such models usually allow such
non-implementable features as punctual tests, perfect clocks, zeno behaviors,
There is therefore a real gap between the usual semantics of models and that of
the implementations, and a natural question is then which of the properties
that have been formally verified on the model carry on to the implementation.
This is the ``robustness'' problem, which we will study in this project.
Of course, the answer to this question depends both on the model semantics and
on the implementation semantics. The latter will thus differ wether we
consider, say, a hardware implementation on circuits or a software
implementation on a real-time operating system. This project addresses both
cases, and that of distributed implementations.
For all of them we will investigate the robustness problem sketched above but
also, linked to control theory, the means to automatically synthesize
implementable correct models and if the latter is not possible for some reason,
we will look how diagnostic theory can be used and extended to allow the safe
execution of an implementation derived from a known non-robust model, by
alerting or taking couter-measures when an unsafe behavior is detected. As a
response to the increasing demand of component-based design, we will also
investigate how robustness can be incorporated in classical compositional
reasoning in the sense that we will try to deduce the robustness of the whole
system from that of its component.
For the conception formalisms, we will also study how semantics alternative to the classical
sequential dense time semantics of time automata, for example, allow to design
more implementable models. To that end, discrete time will of course be
considered as it is closer to our implementation targets semantics. We will
also particularly look into concurrent semantics (unfoldings) to analyze
the specific robustness problems of distributed behaviors.
Finally, we will build on the results obtained in the project and go one step
further by automatically generating code from models we will have proved
implementable. For this task, we will restrict to implementations on a
monoprocessor target running an AUTOSAR OS compliant real-time operating
Monsieur didier lime (ECOLE CENTRALE DE NANTES) – Didier.Lime@ec-nantes.fr
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
IRCCyN ECOLE CENTRALE DE NANTES
ENS Cachan / IRISA ECOLE NORMALE SUPERIEURE DE CACHAN
UPMC/LIP6 UNIVERSITE PARIS VI [PIERRE ET MARIE CURIE]
LSV CNRS - DELEGATION REGIONALE ILE-DE-FRANCE SECTEUR EST
Help of the ANR 359,999 euros
Beginning and duration of the scientific project: - 36 Months