Habilitation à Diriger des Recherches (HDR)

Defense: March 13th, 2014.

Title: High-level Models for Embedded Systems

Jury:

– Gérard Berry (Professeur au Collège de France), Rapporteur
– Rolf Drechsler (Professor at Bremen University, Germany), Rapporteur
– Marco Roveri (Senior Researcher, Fondazione Bruno Kessler, Italy), Rapporteur
– Samarjit Chakraborty (Professor at TU Munchen, Germany), Examinateur
– Benoît Dupont de Dinechin (CTO, Kalray, France), Examinateur
– Frédéric Pétrot (Professor at Grenoble INP, France), Examinateur

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.