Performance Evaluation for Embedded Systems: Between Computationnal
Simulation and Mathematical Solutions
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