WCET: SEmantique, Précision, Traçabilité – W-SEPT

Le flot de développement des applications critiques fait apparaitre 3 niveaux de description : modèles de haut niveau (Matlab/Simulink, Scade), code intermédiaire (C), et enfin code binaire. Découvrir des propriétés fonctionnelles devient de plus en plus difficile quand on avance dans les niveaux. L'approche du projet est de découvrir, transmettre et exploiter des informations au long du flot de conception.

Le résultat principal du projet est une meilleure prise en compte des aspects fonctionnels dans l’évaluation des pires temps d’exécution. Cette démarche est validée par le développement de
démonstrateurs (outils et méthodologie), avec un souci particulier d’intégration aux pratiques utilisées concrètement dans l’industrie. En particulier, les résultats seront mis à la disposition des communautés académique et industrielle via une intégration dans la boîte à outils open-source OTAWA.

Le projet s’inscrit dans le développement et la promotion des techniques statiques d’analyse temporelle. Contrairement aux techniques empiriques basées sur la mesure des temps d’exécution, ce type d’analyse fournit a priori des estimations garanties supérieures. Ce point est particulièrement important dans les domaines critiques (par exemple, avionique) où les systèmes sont soumis à des contraintes de certification.

Le projet a été présenté lors de la réunion de lancement de l’action Timing Analysis on Code-Level (TACLe) du réseau européen COST et au workshop Synchron (http://synchron2012.inria.fr/).
Des publications sont en cours de rédaction et des soumissions sont prévues dans les principales conférences du domaine.

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.