Projet ANR-12-INSE-0001 – W-SEPT : WCET: SEmantique, Précision, Traçabilité
Programme : Ingénierie Numérique & Sécurité (INS) 2012
Année de financement : 2012
Coordinateur du projet : Monsieur Pascal RAYMOND (VERIMAG-Université Joseph Fourier)
Partenaires : CONTINENTAL AUTOMOTIVE FRANCE; Inria Centre Rennes - Bretagne Atlantique; Institut de Recherche en Informatique de Toulouse; Laboratoire Verimag
Montant : 578337.0 euros
Date de début : 2012
Durée : 42 mois
Résumé : Les systèmes embarqués critiques sont généralement constitués d'un ensemble de tâches répétitives
soumises à des contraintes temporelles drastiques (périodes d'échantillonnage, délais de sortie).
Fournir une borne supérieure au pire temps d'exécution (WCET, pour worst-case execution time en anglais),
est donc nécessaire pour prouver la correction du système.
Les méthodes dynamiques, basées sur le test, donnent des résultats réalistes mais non sûrs :
elles ne peuvent pas garantir que le pire cas a effectivement été atteint.
Au contraire, les méthodes statiques d'analyse temporelle calculent des bornes
supérieures sûres au WCET, mais au coût d'une surapproximation potentiellement importante.
Les résultats sont d'ailleurs souvent considérés comme trop pessimistes et irréalistes
pour être utilisés dans beaucoup de secteurs industriels.
Une des plus importantes sources de surapproximation est le manque d'information sémantique sur le
programme. Ce manque d'information conduit l'analyse temporelle à surestimer l'ensemble des exécutions
effectivement réalisables.
Beaucoup d'efforts ont été consacrés à la modélisation fine de la plateforme d'exécution matérielle.
En comparaison, la prise en compte des aspects sémantiques a été beaucoup moins étudiée. Elle
se limite essentiellement à la détermination (nécessaire) des bornes de boucles,
et à l'élimination de chemins infaisables simples. De plus, bien que la méthode IPET
(anglais Implicit Paths Enumeration Technique) soit la plus largement
employée pour le calcul du WCET, il n'existe pas de caractérisation claire de la classe de propriétés sémantiques
qui peuvent être exprimées et exploitées dans son cadre.
La position clé de ce projet est de remettre la sémantique au centre de l'analyse temporelle.
Le but visé est un gain en précision des estimations de WCET. Ce gain doit être atteint
en introduisant de nouvelles stratégies dans les différents niveaux de l'analyse.
En premier lieu, les informations sémantiques pertinentes et utiles à l'amélioration
des estimations vont être caractérisées. Ces informations peuvent être identifiées
depuis le modèle de haut niveau (quand celui-ci existe, comme c'est le cas pour les
conceptions Scade, Simulink etc.), au niveau du code C, ou au niveau du code binaire.
Des solutions pour assurer la traçabilité des informations tout au long du processus de
compilation seront proposées. Enfin, la méthode IPET, issue de l'état de l'art, sera revisitée
pour déterminer jusqu'où elle permet d'exploiter les informations sémantiques qui auront été identifiées.
Des méthodes alternatives seront alors proposées pour faire face à ces limitations.
Toutes ces contributions seront mises en oeuvre dans le cadre de l'outil d'analyse open-source Otawa,
et expérimentées sur des études de cas provenant des domaines spatial et automobile.