Outils formels pour le prototypage virtuel des systèmes embarqués – FOTOVP

Dans le contexte de projets en cours ou pass´es incluant des partenaires industriels de domaines d'application
vari´es, les partenaires de FoToVP ont observ´e plusieurs approches pour le d´eveloppement maˆitris´e
des syst`emes embarqu´es, bas´ees sur la notion de prototype virtuel. Cela nous a permis d'identifier clairement
o`u est le bsoin de m´ethodes formelles. Nous avons commenc´e `a identifier les avantages des m´ethodes
formelles dans les autres projets, avec les contraintes d'un doamine d'application particulier, et des objectifs
pratiques. Des probl`emes r´ecurrents sont apparus. Il nous semble que ces probl`emes n´ecessitent
une recherche amont, ind´ependante d'un domaine d'application particulier, et avec des objectifs pratiques
moins contraignants. Nous proposons d'´etudier ces probl`emes dans FoToVP, pour d´evelopper des
r´esultats g´en´eriques plus fondamentaux. Les motivations sont clairement enracin´ees dans les applications
industrielles ´etudi´ees, et l'applicabilit´e des r´esultats pourra ˆetre ´evalu´ee sur des cas industriels
existants. Les trois domaines que nous avons ´etudi´es sont : – Les syst`emes sur puce, avec STMicroelectronics
– Les r´eseaux de capteurs, avec FranceTelecom R&D – Les syst`emes de contrˆole embarqu´e,
avec EADS, CS, Airbus, RATP, ... Dans tous ces domaines, le cycle de d´eveloppement repose sur la
d´efinition d'un prototype virtuel ex´ecutable, sous la forme d'un mod`ele de haut niveau ex´ecutable. Cette
d´emarche est compliqu´ee par la n´ecessit´e de prendre en compte tous les aspects des syst`emes embarqu´es :
le mat´eriel, le logiciel syst`eme et d'application, la plate-forme d'ex´ecution, et l'environnement physique.
Un tel mod`ele ex´ecutable est bien sˆur utilis´e tout d'abord pour des simulations intensives, pour observer
des propri´et´es fonctionnelles et non fonctionnelles du syst`eme. Mais, comme ces mod`eles apparaissent tˆot
dans le cycle de conception et d´eveloppement, ils deviennent de fait les mod`eles de r´ef´erence. Cela pose
plusieurs probl`emes : – comment construire de tels mod`eles ex´ecutables et formels, suffisamment riches
pour ˆetre utilis´es comme des prototypes virtuels ? – Que signifie la validation formelle de propri´et´es `a
ce niveau ? – Puisque les techniques d'implantation automatique depuis ces mod`eles n'existent pas, comment
comparer un prototype virtuel de haut niveau et une implantation ? – Comment exprimer et valider
des propri´et´es non fonctionnelles au niveau des prototypes virtuels, avec une garantie de r´ealisme des
´evaluations r´ealisables `a ce niveau par rapport aux caract´eristiques du syst`eme final ? Pour r´epondre `a
tous ces probl`emes, nous pensons qu'il faut pouvoir int´egrer dans un cadre g´en´erique de prototypage
virtuel des solutions aux questions suivantes : – Mod´elisation pr´ecise des environnements physiques et
des plates-formes d'ex´ecution – Extraction de mod`eles formels riches et ex´ecutables depuis des langages
non d´efinis formellement mais utilis´es pour le prototypage virtuel, comme SystemC et Java – Abstraction
automatique de ces mod`eles extraits, selon diff´erents crit`eres – Int´egration de code boˆite noire –
Mod´elisation de propri´et´es non fonctionnelles (´energie, ...) – Un cadre formel g´en´eral modulaire pour
composer des mod`eles fonctionnels et non fonctionnels