IRIT - UMR 5505

Dans ce quadriennal, nous avons achevé certains travaux en cours concernant, d’une part les formalismes de spécification et de développement pour le temps réel et la sécurité ; et d’autre part la vérification par analyse statique de systèmes asynchrones. Ainsi, dans le contexte de la méthode B, nous avons conçu une logique temps réel pour le développement basée sur la logique MITL 03-07 [8005] (thèse de M. Rached). Cet enrichissement permet d’introduire des propriétés quantitatives au niveau des spécifications.

Toujours dans le contexte temps réel, nous avons travaillé sur le développement par raffinement d’ordonnanceurs temps réel 03-07 [8463] (thèse d’O. Nasr). La problématique était de dériver du code pour une machine temps réel (possédant des horloges) à partir de spécifications temps réel de haut niveau (e.g. possédant des chronomètres).

Enfin, dans le contexte de la sécurité, nous avons travaillé sur la combinaison des logiques temporelle et déontique 04-07 [8883] (thèse de J. Brunel). Ce dernier travail est aujourd’hui terminé et nous ne poursuivons plus cet axe de réflexion.

Dans le contexte de systèmes répartis asynchrones, nous avons complété les analyses statiques définies précédemment basées sur le flot de données (inférence de type et résolution de contraintes multi-ensemblistes [2848,5744]) par une approche basée sur le flot de contrôle à base d’interprétation abstraite [8416] (thèse de P-L. Garoche).

D’autre part, nous nous sommes concentrés sur l’assistance au développement de systèmes critiques temps réel à travers la définition et l’implantation de langages dédiés, de transformations correctes vers des outils de vérification et vers du code source. Nous abordons les facettes fonctionnelles et architecturales dans les domaines asynchrone et synchrone. Ces deux facettes se sont concrétisées autour de deux groupes de projets structurants, d’une part TOPCASED, OpenEmbeDD, SPICES, TAPIOCA, SYMPASS, CESAR et quarteFt, et d’autre part GeneAuto, SPaCIFY, CESAR et OPEES.

Langages dédiés et transformations

En ce qui concerne les langages dédiés, un point essentiel est la possibilité d’exprimer les différentes formes de sémantiques de ces langages et d’exploiter celles-ci pour la construction de moyens de validation et vérification des modèles, et pour la preuve de la correction de transformations. Notre contribution se situe au niveau de la définition d’un patron de métamodélisation pour rendre exécutable un langage de modélisation dédié (DSML) défini par un métamodèle statique (thèse de B. Combemale 06-08 [10165]). Pour illustration, une chaîne complète de vérification a été développée pour SimplePDL, un langage de description de procédé, vers les réseaux de Petri et les outils Tina développés par l’équipe OLC du LAAS. Il est ensuite nécessaire de vérifier la correction de cette transformation. Nous avons développé pour cela une formalisation spécifiée en Coq des notions réflexives de modèles et méta-modèles. Nous avons également expérimenté différentes approches pour spécifier et vérifier des transformations de modèles dans des assistants de preuve (thèses de N. Izerrouken 07-, C. Picard 08-, M. Giorgino 08-).

Modélisation et vérification asynchrone

Pour la modélisation et la vérification en approche asynchrone, nous avons travaillé :

• sur la définition de la sémantique de modèles d’exécution temps réel. Nous nous sommes intéressés au langage AADL (thèse de L. Pi 06-).

• sur la notion de mode. Il s’agit là d’une notion essentielle qui permet une souplesse dans la définition de configurations logicielles tout en préservant l’aspect statique nécessaire pour l’analyse (thèse de J-F. Rolland 04-08 [10290]).

Ces études sont à la base de nos activités concernant les langages de modélisation temps réel et plus particulièrement AADL. Pour exprimer la sémantique des concepts sous-jacents et permettre la vérification de modèle, nous avons défini le langage Fiacre en collaboration avec les collègues de l’équipe OLC du LAAS et de l’équipe VASY de l’INRIA (Grenoble). Fiacre est un langage de processus communicants temps réel asynchrone basé sur les systèmes de transitions temporisées. L’équipe a plus particulièrement participé à la définition de la sémantique des constructions temps réel du langage AADL, à la définition et à l’outillage de l’annexe comportementale du langage AADL (en cours de discussion au sein du comité de standardisation du SAE). Dans la chaîne de traduction permettant la vérification de modèles AADL, notre contribution a porté sur la traduction de AADL vers Fiacre dont un prototype est aujourd’hui opérationnel. Des expérimentations avec des collègues brésiliens de l’UFSC ainsi qu’avec des industriels ont été menées.

Modélisation et vérification synchrone

Pour la modélisation et la vérification en approche synchrone, nous avons travaillé sur la formalisation de la sémantique du langage Simulink/Stateflow exploité par de nombreux partenaires industriels et sur la construction d’outils de vérification et de génération de code certifié en s’appuyant sur des méthodes formelles. Cette sémantique prend en compte les aspects flots de données et flots de contrôle de manière plus précise que les plongements usuels dans les langages synchrones et permet de préserver l’intention du concepteur en terme d’ordonnancement. Ceci constitue la première originalités de ces travaux. La seconde est l’interaction avec les autorités de certification pour définir un processus qualifiable à base de méthodes formelles. Ces travaux se déroulent dans les thèses de N. Izerrouken 07- et d’A. Toom 08- co-encadrement TTU.

La combinaison des deux approches synchrones et asynchrones se concrétise par la définition du langage SYNOPTIC en collaboration avec l’équipe ESPRESSO de l’IRISA. SYNOPTIC est dédié à la construction d’applications embarquées dans le domaine satellitaire et du processus de développement associé. SYNOPTIC est basé sur GeneAuto pour la spécification fonctionnelle et AADL pour la description de l’architecture matérielle.