Implementabilty and Robustness of Timed Systems – ImpRo

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,
etc.

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
system.