Amphi H, Ensimag
13 March 2014 - 14h00
High-level Models for Embedded Systems (HDR)
by Matthieu Moy from Verimag
Abstract: Modern embedded systems have reached a level of complexity such that
it is no longer possible to wait for the first physical prototypes
to validate choices on the integration of hardware and software
components. It is necessary to use models, early in the design flow.
The work presented in this document contribute to the state of the
art in several domains.
First, we present some verification techniques based on abstract
interpretation and SMT-solving for programs written in
general-purpose languages like C, C++ or Java.
Then, we use verification tools on models written in SystemC at the
transaction level (TLM). Several approaches are presented, most of
them using compilation techniques specific to SystemC to turn the
models into a format usable by existing tools.
The second part of the document deal with non-functional properties
of models: timing performances, power consumption and temperature.
In the context of TLM, we show how functional models can be enriched
with non-functional information.
Finally, we present contributions to the modular performance
analysis (MPA) with real-time calculus (RTC) framework. We describe
several ways to connect RTC to more expressive formalisms like timed
automata and the synchronous language Lustre. These connections
raise the problem of causality, which is defined formally and solved
with the new causality closure algorithm.
Composition du jury :
- Gérard Berry (Professeur au Collège de France), Rapporteur
- Rolf Drechsler (Professeur à l'Université de Brême, Allemagne), Rapporteur
- Marco Roveri (Senior Researcher, Fondazione Bruno Kessler, Italie), Rapporteur
- Samarjit Chakraborty (Professeur à l'université technique de Munich, Allemagne), Examinateur
- Benoît Dupont de Dinechin (Directeur Technique, Kalray, France), Examinateur
- Frédéric Pétrot (Professeur à Grenoble INP, France), Examinateur
