4 Subjects, M2R / M1 2010-2011, Verimag

Scientific Context:

Modern embedded systems design must deal with more and more constraints in sereval domains: systems are more and more complex, but have to be manufactured at low cost, and with an increasingly short lifecycle.

In this context, it is no longer possible to wait for the physical prototypes to validate the decisions on the conception of a system, it is necessary to use a model (i.e. an abstract representation of the system, but not yet an implementation) as early as possible in the design flow.

We are interested in the performance study (processing time, and if possible energy consumed) on models of embedded systems.

Simulation. The laboratory already has a good experience in the study of fine-grained models, expressed as programs that we can execute to simulate the complete behavior of a system, and obtain some performance information.

Analytical Solution. As opposed to this, there exists purely analytical models, based on mathematical equations that can be solved efficiently. These models can represent in a simple way the amount of events to process and how fast they can be processed. Solving these equations can give, for example, the best and worst cases for performances.

The approach we are interested in here is called "Real-Time Calculus", or RTC. It allows the characterization in streams of events with curves giving worst and best cases on the number of events per unit of time. A system can be described with a curve for its input stream and another curve for its output stream. The huge advantage of RTC is its ability, for simple components, to give exact bounds on the output stream of a component as a function of its input stream. Unfortunately, complex components can not be modeled in RTC, so we need to find a way to use other techniques for these components.

Combining Simulation and Analytical Solutions. We started experimenting with the use of classical formal verification techniques (such as abstract interpretation and model-checking) applied to models described in RTC. We already have the theoritical foundations and a prototype to design the models and the mathematical objects used in RTC with the Lustre language in order to analyze them.

Subjects:

1) Last year, we proposed a canonical form for the RTC curves, called
"causal": in order to justify our analysis, the RTC curves should be
causal. For the moment, we have algorithms that transforms curves for
some simple encodings of curves. We wish to extend the algorithms to be
able to handle more complex encodings and then to implement them into
the tool chain.

2) The performance analysis is performed using connection to external
tools from abstract interpretation and model-checking. The efficiency
of the analysis is thus often critical, but highly correlated to the
tools: we wish to use a new abstract interpretation tool which would
fit better the RTC properties. This work is not only a matter of
connection between tools, it also implies to modify the models and the
properties under analysis for the new tool.

3) A similar approach was done by a research team for ETH Zurich. They
model the system under analysis and RTC curves as timed automata and
then perform the analysis with a model-checking tool. The first tests
we did showed that the two approaches are not directly comparable: we
need to design a case study in order to better compare the approaches
and to decide the criteria for which an approach is efficient. This
work would be done in collaboration with the team in Zurich.

4) Complex components can not be modeled using the RTC formalism. The
global aim of the previous subjects is to extend the formalism using
formal methods (model-checking, abstract interpretation). Another way
to obtain this goal is to change the RTC formalism and to propose a new
abstraction to describe the flows of events. This subject is divided in
three steps:

- Define a formalism, based on the notion of automata,
allowing the representation of an event flow.

- Define the way to compute the abstraction of an output flow produced
by a module, as a function of the information available on its input,
and a model of the module's behavior.

- Implement these algorithms and apply them on several examples.

For any subjects, the expected work include a bibliographical study on modeling of embedded systems for performance evaluation (simulation models, RTC), concrete experimentation (and therefore an implementation of the proposed algorithms), and a comparison with RTC. Those subjects make a bridge between programming for simulation and formal study of the same systems. It includes theoretical and practical points. Don't hesitate to come and discuss the subject!

Working environment:

The student will work within the SYNCHRONE team of the Verimag laboratory.

Continuing with a Ph.D thesis on a related topic is possible.

Contacts:

Karine Altisen,

Matthieu Moy