|
|
Outils formels pour le
prototypage virtuel
des
systèmes embarqués
|
- prototypage virtuel,
- systèmes embarqués,
- composants,
- langages synchrones, langages d'ingénierie (SystemC, ...)
|
 |
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.
|
|
