@article{Moy14b,
title = { {Compte-rendu d'habilitation : Mod{\'e}lisation {\`a} haut niveau d'abstraction pour les syst{\`e}mes embarqu{\'e}s} },
author = {Moy, Matthieu},
year = {2014},
journal = {Technique et Science Informatiques},
number = {3},
pages = {285-293},
volume = {33},
team = {SYNC},
hal_id = {hal-00986536},
language = {Fran{\c c}ais},
affiliation = {VERIMAG - IMAG},
pdf = {http://hal.archives-ouvertes.fr/hal-00986536/PDF/hdr-matthieu-moy-fr.pdf},
abstract = {{Les syst{\`e}mes embarqu{\'e}s modernes ont atteint un niveau de complexit{\'e} qui fait qu'il n'est plus possible d'attendre les premiers prototypes physiques pour valider les d{\'e}cisions sur l'int{\'e}gration des composants mat{\'e}riels et logiciels. Il est donc n{\'e}cessaire d'utiliser des mod{\`e}les, t{\^o}t dans le flot de conception. Les travaux pr{\'e}sent{\'e}s dans ce document contribuent {\`a} l'{\'e}tat de l'art dans plusieurs domaines. Nous pr{\'e}sentons dans un premier temps de nouvelles techniques de v{\'e}rification de programmes {\'e}crits dans des langages g{\'e}n{\'e}ralistes comme C, C++ ou Java. Dans un second temps, nous utilisons des outils de v{\'e}rification formelle sur des mod{\`e}les {\'e}crits en SystemC au niveau transaction (TLM). Plusieurs approches sont pr{\'e}sent{\'e}es, la plupart d'entre elles utilisent des techniques de compilations sp{\'e}cifiques {\`a} SystemC pour transformer le programme SystemC en un format utilisable par les outils. La seconde partie du document s'int{\'e}resse aux propri{\'e}t{\'e}s non-fonctionnelles des mod{\`e}les : performances temporelles, consommation {\'e}lectrique et temp{\'e}rature. Dans le contexte de la mod{\'e}lisation TLM, nous proposons plusieurs techniques pour enrichir des mod{\`e}les fonctionnels avec des informations non-fonctionnelles. Enfin, nous pr{\'e}sentons les contributions faites {\`a} l'analyse de performance modulaire (MPA) avec le calcul temps-r{\'e}el (RTC). Nous proposons plusieurs connections entre ces mod{\`e}les analytiques et des formalismes plus expressifs comme les automates temporis{\'e}s et le langage de programmation Lustre. Ces connexion posent le probl{\`e}me th{\'e}orique de la causalit{\'e}, qui est formellement d{\'e}fini et r{\'e}solu avec un algorithme nouveau dit de " fermeture causale ".}},
}
