Exécution embarquée de modèles avec un interpréteur EMI

Définition

En informatique comme en linguistique, un langage est défini par sa syntaxe et sa sémantique. La syntaxe caractérise l’ensemble des concepts du langage et leurs représentations concrètes. La sémantique permet quant à elle d’associer une signification à chaque élément syntaxique du langage. Ces deux notions permettent de définir la forme (la structure et la notation) et le fond (le sens) des programmes [Com08]. Pour les langages de programmation, on dissocie la syntaxe abstraite de la syntaxe concrète. La syntaxe abstraite définit l’ensemble des concepts (ou constructions) du langage et leurs relations. Elle ne s’intéresse donc qu’à la structure interne des programmes. Elle peut par exemple être définie à l’aide d’une grammaire et ainsi se représenter sous la forme d’un arbre syntaxique (ou en anglais Abstract Syntax Tree (AST)). Les noeuds de l’arbre correspondent alors aux constructions du langage et les branches aux arguments de ces constructions. La syntaxe concrète permet quant à elle d’associer une représentation à chacun des concepts du langage. C’est cette représentation concrète qui sera utilisée par les ingénieurs pour définir des programmes dans ce langage. Elle peut prendre une forme textuelle (p. ex. avec Xtext [EB10], TCS [JBK06]) ou graphique (p. ex. avec Sirius 1).

Dans le cas d’une représentation textuelle, la syntaxe concrète est typiquement définie à l’aide d’une grammaire pouvant ensuite être utilisée par un parseur pour construire l’arbre syntaxique d’un programme. Un langage est aussi caractérisé par son domaine sémantique qui représente l’ensemble des états atteignables d’un programme [Com08] (c.-à-d. l’ensemble des combinaisons de valeurs pouvant être prises par les attributs dynamiques d’un programme). La sémantique d’un langage définit comment passer d’un état à un autre (c.-à-d. l’évolution des valeurs des attributs dynamiques d’un programme). Un langage informatique repose donc sur la combinaison de trois éléments : une syntaxe abstraite, une syntaxe concrète et un domaine sémantique. La définition d’un langage est centrée soit sur sa syntaxe concrète soit sur sa syntaxe abstraite. Des liens (Mca, Mcs) ou (Mac, Mas) permettent d’associer les concepts de la syntaxe concrète ou de la syntaxe abstraite avec les concepts des autres éléments. Ces deux possibilités sont illustrées sur la Figure 1.1.

syntaxe abstraite (en bleu). (Figure adaptée de [Com08]) Pour des raisons historiques, les langages dont la définition est axée sur la syntaxe concrète sont principalement des langages de programmation. Un lien Mca dit de dérivation ou d’abstraction permet d’associer les éléments de la syntaxe concrète à ceux de la syntaxe abstraite. Ce lien est souvent obtenu via l’utilisation d’un parseur. Celui-ci permet d’enlever tout le sucre syntaxique (p. ex. les accolades, les points-virgules) servant uniquement à la mise en forme du programme. Un lien Mcs permet de lier les concepts de la syntaxe concrète avec des états (ou des valeurs) du domaine sémantique du langage. Définition 1.1 (Langage centré sur la syntaxe concrète). “Un langage informatique est défini selon le tuple {AS,CS,Mca, SD,Mcs} où AS est la syntaxe abstraite, CS est la syntaxe concrète, Mca est le mapping de la syntaxe concrète vers sa représentation abstraite, SD est le domaine sémantique et Mcs est le mapping de la syntaxe concrète vers le domaine sémantique.” [Com08] La définition d’un langage peut également être centrée sur sa syntaxe abstraite. L’utilisation de cette définition est privilégiée par les langages de modélisation. Elle permet notamment l’usage de multiples syntaxes concrètes offrant ainsi la possibilité d’utiliser différents formalismes pour différents besoins.

Pour la modélisation, certains utilisateurs préfèrent un formalisme graphique alors que d’autres sont plus à l’aise avec un formalisme textuel. Pour le stockage des programmes, il peut également être intéressant d’utiliser un formalisme dédié (p. ex. XML Metadata Interchange (XMI®) [OMG15]) pour favoriser l’interopérabilité entre les outils. Pour chaque syntaxe concrète, la définition du langage doit donc fournir un lien Mac entre les concepts de la syntaxe abstraite et les décorations syntaxiques (graphiques ou textuelles) utilisées dans la syntaxe concrète. Un seul lien Mas est cependant nécessaire pour lier les concepts de la syntaxe abstraite avec des états (ou des valeurs) du domaine sémantique du langage. Définition 1.2 (Langage centré sur la syntaxe abstraite). “Un langage informatique est défini selon le tuple {AS,CS_,M_ ac, SD,Mas} où AS est la syntaxe abstraite, CS_ est la (les) syntaxe(s) concrète(s), M_ ac est l’ensemble des mappings de la syntaxe abstraite vers la (les) syntaxe(s) concrète(s), SD est le domaine sémantique et Mas est le mapping de la syntaxe abstraite vers le domaine sémantique.” [Com08] Dans cette thèse, nos travaux se focalisent sur l’exécution et l’analyse dynamique de programmes. Après avoir défini la notion de langage, notre intérêt se porte donc sur la définition de la sémantique des langages.

Outils

Dans la communauté du génie logiciel, de nombreux outils ont été développés pour capturer la sémantique d’un langage de façon translationnelle. En pratique, ces outils ne traduisent pas les modèles directement vers du code machine mais vers un langage intermédiaire ayant un niveau d’abstraction plus ou moins élevé. Plusieurs étapes de traduction sont donc nécessaires avant d’obtenir du code machine qui soit exécutable par une plateforme d’exécution matérielle.

Différents niveaux d’abstraction. Pour classifier les générateurs de code, cette thèse propose de les regrouper en trois grands groupes dépendants essentiellement du niveau d’abstraction du langage cible. Vers un GPL. Une première méthode est de définir un générateur de code vers un langage de programmation générique (GPL) (p. ex. C, C++, Java, Objective-C, Ada). De nombreux outils ont notamment été définis pour UML dont Papyrus Software Designer (Papyrus SD) [Pha+17], Rhapsody [HK04], Rational Software Architect (RSA) [LNH06], UML4CPP [Jäg+16] ou le simulateur UML [KDH07]. Concernant les systèmes temps réel, les outils Fujaba [Bur+05], Rational Software Architect Real Time Edition (RSARTE) [Moh15] et Papyrus-RT [HDB17] permettent de générer du code prenant en compte des contraintes temps réel. Vers une représentation intermédiaire dédiée. Une autre approche propose de transformer le modèle de conception vers un langage intermédiaire plus proche des concepts d’implémentation. Les travaux [PM03a; PM03b; SM05b] reposent sur cette approche pour exécuter des modèles UML en passant par les formalismes intermédiaires Extended Hierarchical Automata (EHA) [PM03a; PM03b] ou Executable State Machine (ESM) [SM05b]. L’intérêt de ces formalismes est notamment de mettre à plat les machines à états UML pour simplifier la génération de code [PM03a; PM03b] ou rendre l’exécution plus efficace [SM05b].

Vers un langage assembleur. D’autres générateurs de code, souvent qualifiés de compilateurs, ont été définis vers des langages bas niveau (c.-à-d. très proche du langage machine). Des compilateurs existent notamment pour les langages de programmation comme C (p. ex. GCC) ou Rust (p. ex. rustc). Pour UML, les compilateurs de modèles GUML [CMB12] et Unicomp [Cic18] permettent de transformer des modèles UML vers du code binaire en passant par une représentation intermédiaire de GCC3 ou LLVM4. Tous ces outils permettent d’exécuter des modèles et sont généralement adaptés pour l’exécution embarquée. En ce qui concerne plus spécifiquement UML, la section A.3.3 donne un aperçu des outils implémentant une sémantique translationnelle pour UML. Parmi tous ces outils, très peu utilisent une approche formelle. En particulier, aucun des outils cités précédemment ne permet de garantir que le code exécutable obtenu est conforme au modèle de conception initial. Pour le langage UML, il n’existe pas, à notre connaissance, d’outils permettant de remplir cet objectif. Dans la littérature, plusieurs travaux [LP99; Fra+98; Liu+13a] ont proposé une définition formelle de la sémantique d’UML en se basant sur une notation mathématique. Néanmoins, ces définitions formelles servent uniquement à appliquer des activités d’analyse sur des modèles UML mais pas à exécuter ces modèles sur des plateformes d’exécution réelles.

Garantir la sémantique d’exécution. Plusieurs outils permettent de garantir que la sémantique d’exécution est conforme à la sémantique du langage de modélisation. Il est par exemple intéressant de noter l’initiative du projet CompCert 5 [Ler09] qui a permis de construire le premier compilateur de code C certifié en utilisant Coq 6 [BC10]. Pour les systèmes embarqués, l’environnement de développement SCADE [Ber07] possède quant à lui un générateur de code certifié, appelé KCG compiler, pour rendre exécutable les modèles SCADE. En couplant Comp- Cert avec le générateur de code KCG, il serait possible de garantir que la sémantique d’exécution des modèles SCADE est conforme à sa spécification. Dans le cadre de l’ingénierie des modèles, il est également intéressant de mentionner l’approche en [Com+09]. Elle permet de définir une sémantique translationnelle pour un langage de modélisation donné et de valider celle-ci par rapport à une sémantique opérationnelle de référence grâce aux techniques de bisimulation.

Table des matières

Introduction
Contexte
Problématiques
Contributions
Plan du manuscrit
Liste des publications
I État de l’art
1 L’exécution de programmes
1.1 Introduction
1.2 Définition d’un langage
1.2.1 Définition
1.2.2 Sémantique structurelle vs comportementale
1.2.3 Les différents styles de définition de la sémantique comportementale
1.2.3.1 Sémantique opérationnelle
1.2.3.2 Sémantique dénotationnelle
1.2.3.3 Sémantique translationnelle
1.2.3.4 Sémantique axiomatique
1.3 Approches pour l’exécution de programmes
1.3.1 Définition des relations “conforme à” et “implémente”
1.3.2 Approches basées sur une sémantique translationnelle
1.3.2.1 Description
1.3.2.2 Outils
1.3.3 Approches basées sur une sémantique opérationnelle
1.3.3.1 Description
1.3.3.2 Outils
1.3.4 Synthèse
2 L’analyse et la vérification de programmes 31
2.1 Introduction
2.2 Panorama des techniques de V&V
2.3 Vérification formelle
2.3.1 Principes
2.3.2 Preuve d’équivalence
2.4 Le model-checking
2.4.1 Principes du model-checking
2.4.2 Mise en oeuvre du model-checking
2.4.3 Avantages et limites du model-checking
2.5 Approches pour l’analyse et la vérification logicielle
2.5.1 Approches par raffinement
2.5.1.1 Description
2.5.1.2 Langages et outils
2.5.2 Approches avec une transformation vers un langage d’analyse
2.5.2.1 Description
2.5.2.2 Langages et outils
2.5.3 Approches d’analyse dédiées au langage
2.5.3.1 Description
2.5.3.2 Outils
2.5.4 Approches d’analyse par API
2.5.4.1 Description
2.5.4.2 Outils et protocoles
2.6 Synthèse
3 Approches pour l’exécution et l’analyse de modèles
3.1 Introduction
3.2 Contexte de développement
3.3 Problèmes pour l’analyse et l’exécution réelle
3.3.1 Fossés sémantiques
3.3.2 Problème d’équivalence
3.4 Approche 1 : traduction vers modèle vérifiable et code
3.5 Approche 2 : traduction vers modèle vérifiable puis code
3.6 Approche 3 : traduction vers code vérifiable
3.7 Approche 4 : traduction modèle vérifiable vers code
3.8 Approche 5 : raffinement de modèles jusqu’au code
3.9 Approche 6 : interprétations spécifiques pour vérification et exécution réelle
3.10 Analyse des six approches
3.11 Approche X : interprétation unifiée pour vérification et exécution réelle
3.12 Objectifs de recherche
3.13 Synthèse
II L’approche EMI
4 Présentation de l’approche EMI
4.1 Introduction
4.2 Description de l’architecture candidate
4.3 Un contrôleur d’exécution pour chaque activité
4.4 L’interface STR
4.5 Analyse de modèles avec un interpréteur EMI
4.6 Exécution embarquée de modèles avec un interpréteur EMI
4.7 Présentation des différents modes d’exécution
4.8 Synthèse
5 Analyse de l’exécution de modèles 80
5.1 Introduction
5.2 Abstraction de l’environnement
5.3 Simulation, débogage, et détection de deadlocks
5.3.1 Simulation interactive
5.3.2 Débogage multivers
5.3.3 Détection de deadlocks
5.4 Architecture de vérification formelle
5.4.1 Automates de Büchi et automates observateurs
5.4.2 Les interfaces APC et Acc
5.4.3 Description de l’architecture conceptuelle
5.4.4 Architecture conceptuelle pour le model-checking
5.4.5 Architecture conceptuelle pour le monitoring
5.5 Composition synchrone
5.5.1 Description théorique
5.5.2 Optimisation pour le monitoring
5.6 Model-checking avec des propriétés LTL
5.6.1 Spécification de propriétés LTL
5.6.2 Architecture logicielle pour la vérification LTL
5.7 Synthèse
6 L’ordonnancement pour la vérification et l’exécution embarquée de modèles
6.1 Introduction
6.2 Non-déterminisme
6.3 Formalisation des opérateurs
6.3.1 Opérateur de filtrage
6.3.2 Opérateur d’ordonnancement
6.3.3 Opérateur de composition asynchrone
6.4 Vérification formelle et exécution embarquée avec ordonnancement
6.4.1 Exécution réelle
6.4.2 Model-checking avec filtrage
6.4.3 Model-checking avec l’ordonnanceur dans la boucle de vérification
6.4.4 Model-checking avec un environnement découplé
6.5 Synthèse
7 Pilotage et observation de l’exécution de modèles
7.1 Introduction
7.2 Pilotage de l’interpréteur
7.3 Le langage d’observation
7.3.1 Présentation du langage d’observation
7.3.2 Les opérateurs du langage d’observation
7.3.3 Évaluation des prédicats
7.4 Architecture logicielle d’analyse avec un interpréteur EMI
7.4.1 Description de l’architecture logicielle
7.4.2 Le serveur de langages
7.4.3 Canonisation de la configuration
7.5 Synthèse
8 Conception d’un interpréteur de modèles embarqué et pilotable
8.1 Introduction
8.2 Méthodologie de conception
8.3 Métamodélisation
8.3.1 Métamodélisation du langage de conception
8.3.2 Métamodélisation des données d’exécution
8.3.3 Le modèle objet et l’instanciation
8.3.4 La notion de configuration
8.3.5 Sérialisation des métamodèles
8.4 Implémentation de la sémantique opérationnelle
8.4.1 Implémentation d’une sémantique pilotable
8.4.2 Une sémantique utilisable en vérification formelle
8.5 Chargement du modèle
8.6 Déploiement sur la plateforme d’exécution
8.7 Synthèse
9 Unification du model-checking et du monitoring de spécifications UML exécutables
9.1 Introduction
9.2 Expression de propriétés dans le langage de modélisation
9.2.1 Modélisation de propriétés en UML
9.2.2 Modélisation des automates de Büchi en UML
9.2.3 Modélisation des automates observateurs en UML
9.2.4 Conversion des propriétés LTL en PUSMs
9.3 Composition synchrone
9.3.1 Mise en oeuvre de la composition synchrone
9.3.2 Ajout de transitions implicites
9.3.3 Composition synchrone avec un automate de Büchi
9.3.4 Composition synchrone avec un automate observateur
9.4 Model-checking et monitoring avec des machines à états UML
9.4.1 Architecture de model-checking avec des PUSMs
9.4.2 Architecture de monitoring avec des PUSMs
9.5 Synthèse
III Évaluation de l’approche
10 Expérimentations
10.1 Introduction
10.2 Présentation de l’outil EMI-UML
10.3 Présentation des cas d’études
10.3.1 Contrôleur de passage à niveau
10.3.2 Interface d’un régulateur de vitesse
10.4 Mise en oeuvre des activités d’analyse de modèles
10.4.1 Simulation interactive
10.4.2 Débogage multivers
10.4.3 Model-checking LTL et détection de deadlocks
10.4.4 Model-checking avec l’ordonnanceur
10.4.5 Model-checking avec des PUSMs
10.4.5.1 Spécification de PUSMs
10.4.5.2 Model-checking du comportement du système
10.4.6 Model-checking des mécanismes de sûreté de fonctionnement
10.4.7 Exécution embarquée et monitoring
10.4.8 Évaluation des performances d’exécution
10.5 Expérimentations avec d’autres outils
10.5.1 EMI-LOGO : un interpréteur de modèles LOGO
10.5.2 AnimUML : un outil d’interprétation et d’animation de modèles UML
10.5.3 Intégration d’EMI-UML dans Gemoc Studio
10.6 Synthèse des expérimentations
10.7 Contributions scientifiques
10.7.1 C#1 Contribution à l’unification de l’analyse et de l’exécution embarquée de modèles
10.7.2 C#2 Contribution à l’adoption des techniques de vérification formelle par les ingénieurs
10.8 Synthèse
Conclusion
Rappel du contexte et des problèmes considérés
Solution proposée
Perspectives
Bibliographie
Annexes
A Le langage UML et ses fondements en IDM
A.1 Introduction
A.2 L’ingénierie dirigée par les modèles
A.2.1 Principes de l’IDM
A.2.1.1 Les relations clés de l’IDM
A.2.1.2 L’approche MDA
A.2.1.3 Transformation de modèles
A.2.2 Les langages en IDM
A.3 Le langage UML
A.3.1 Historique
A.3.2 Le standard UML
A.3.3 Techniques d’exécution de modèles UML
A.3.4 Techniques d’analyse de modèles UML
A.4 Synthèse
B Formalisation en Lean
C Langage d’action et langage d’observation pour les modèles UML
C.1 Langage d’expression
C.2 Langage d’effet
C.3 Extension du langage d’expression
D Présentation des cas d’études
D.1 Contrôleur de passage à niveau
D.2 Interface du régulateur de vitesse
E Liste des propositions atomiques
E.1 Liste des propositions atomiques pour le modèle du contrôleur de passage à
Niveau
E.2 Liste des propositions atomiques pour le modèle d’interface du régulateur de
Vitesse
F Pages web archivées
Acronymes
Table des figures
Liste des tableaux
Liste des listings