An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language

• Main Author: Stöcker, Jan
• Language: ENG
• Published: 2009
• Subjects: [INFO:INFO_MO] Computer Science/Modeling and Simulation; algèbre de processus; automate; concurrence; méthode formelle; modèle intermédiaire; temps-réel; réseau de Petri; vérification
• Online Access: http://tel.archives-ouvertes.fr/tel-00551724; http://tel.archives-ouvertes.fr/docs/00/55/17/24/PDF/thesis_stoecker.pdf

La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple Uppaal) et les réseaux de Petri temporisés (par exemple Tina). Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non-temporisés qui manipulent des données complexes. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec Uppaal) et vers des réseaux de Petri temporisés (pour la vérification avec Tina). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple.