FoToVP



Ce projet fait partie du programme ARA SETIN
This project belongs to the ARA SETIN programme.

 







 

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

Mots Clés

  • prototypage virtuel,
  • systèmes embarqués,
  • composants,
  • langages synchrones, langages d'ingénierie (SystemC, ...)
English version

Résumé

Dans le contexte de projets en cours ou passés incluant des partenaires industriels de domaines d'application variés, les partenaires de FoToVP ont observé plusieurs approches pour le développement maîtrisé des systèmes embarqués, basées sur la notion de prototype virtuel. Cela nous a permis d'identifier clairement où est le bsoin de méthodes formelles. Nous avons commencé à identifier les avantages des méthodes formelles dans les autres projets, avec les contraintes d'un doamine d'application particulier, et des objectifs pratiques. Des problèmes récurrents sont apparus. Il nous semble que ces problèmes nécessitent une recherche amont, indépendante d'un domaine d'application particulier, et avec des objectifs pratiques moins contraignants. Nous proposons d'étudier ces problèmes dans FoToVP, pour développer des résultats génériques plus fondamentaux. Les motivations sont clairement enracinées dans les applications industrielles étudiées, et l'applicabilité des résultats pourra être évaluée sur des cas industriels existants. Les trois domaines que nous avons étudiés sont :
  • Les systèmes sur puce, avec STMicroelectronics
  • Les réseaux de capteurs, avec FranceTelecom R&D
  • Les systèmes de contrôle embarqué, avec EADS, CS, Airbus, RATP, ...
Dans tous ces domaines, le cycle de développement repose sur la définition d'un prototype virtuel exécutable, sous la forme d'un modèle de haut niveau exécutable. Cette démarche est compliquée par la nécessité de prendre en compte tous les aspects des systèmes embarqués : le matériel, le logiciel système et d'application, la plate-forme d'exécution, et l'environnement physique. Un tel modèle exécutable est bien sûr utilisé tout d'abord pour des simulations intensives, pour observer des propriétés fonctionnelles et non fonctionnelles du système. Mais, comme ces modèles apparaissent tôt dans le cycle de conception et développement, ils deviennent de fait les modèles de référence. Cela pose plusieurs problèmes :
  • comment construire de tels modèles exécutables et formels, suffisamment riches pour être utilisés comme des prototypes virtuels ?
  • Que signifie la validation formelle de propriétés à ce niveau ?
  • Puisque les techniques d'implantation automatique depuis ces modèles n'existent pas, comment comparer un prototype virtuel de haut niveau et une implantation ?
  • Comment exprimer et valider des propriétés non fonctionnelles au niveau des prototypes virtuels, avec une garantie de réalisme des évaluations réalisables à ce niveau par rapport aux caractéristiques du système final ?
Pour répondre à tous ces problèmes, nous pensons qu'il faut pouvoir intégrer dans un cadre générique de prototypage virtuel des solutions aux questions suivantes :
  • Modélisation précise des environnements physiques et des plates-formes d'exécution
  • Extraction de modèles formels riches et exécutables depuis des langages non définis formellement mais utilisés pour le prototypage virtuel, comme SystemC et Java
  • Abstraction automatique de ces modèles extraits, selon différents critères
  • Intégration de code boîte noire
  • Modélisation de propriétés non fonctionnelles (énergie, ...)
  • Un cadre formel général modulaire pour composer des modèles fonctionnels et non fonctionnels

Résultats scientifiques et techniques attendus

  • Une image globale de la démarche de prototypage virtuel, d'un point de vue formel. Nous décrirons un cadre global pour l'assemblage de composants qui modélisent les parties d'un système complexe (matériel, logiciel, système d'exploitation, etc.). La sémantique de l'assemblage doit prendre en compte à la fois les aspects fonctionnels et non fonctionnels. Nous définirons également une forme unifiée pour les composants individuels, exprimant les aspects fonctionnels et non fonctionnels. L'idée est de définir une forme adéquate aussi bien pour les modèles du matériel que pour des portions de code détaillées, ou pour des modèles d'environnements physiques. Finalement, nous définirons une relation ``est plus précis'' sur ces modèles individuels, permettant de manipuler des abstractions. Les composants et leurs assemblages seront exécutables.
  • Des outils pour l'extraction de modèles formels depuis des langages industriels, et pour l'abstraction automatique de ces modèles.
  • Plus généralement, un progrès dans notre compréhension des approches et solutionsa courantes, dans divers domaines d'application.

Résultats industriels et économiques attendus

Du côté industriel, bien que nos objectifs ici ne soient pas de produire des résultats directement utilisables, les racines du projet sont clairement inspirées de cas d'étude industriels. Les résultats fondamentaux et génériques que nous développerons devraient constituer une bonne base pour du travail plus appliqué ultérieur.