Nous nous intéressons aux approches formelles pour le développement de systèmes réactifs critiques. Le langage synchrone Lustre pour la spécification de tels systèmes a subit des évolutions majeurs au cours des dernières années en intégrant dans sa sémantique à base flots de données synchrones des constructions de plus haut-niveau appelées automates de modes (dans le langage Scade 6). Ceux-ci mettent en œuvre l'activation de modes de calculs en fonction des états et des transitions de l'automate, et reposent pour cela sur la sémantique des horloges du langage Lustre. En particulier, nous étudiions la prise en compte des horloges et des automates de modes dans l'outil de génération de tests GATeL dédié à l'origine au langage Lustre mono-horloge (flots de données purs). GATeL génère automatiquement des séquences de tests pour un modèle à partir d'un objectif de test décrit en Lustre à travers une exploration en arrière des dépendances entre flots et selon des teniques de résolution de contraintes. Nous présentons ces différents domaines et la mise en oeuvre des modifications apportées à l'outil pour prendre en compte les automates de modes. Enfin, nous définissons des critères de couverture structurelle pour les automates de modes et montrons alors comment, en les traduisant de manière automatique sous forme d'objectifs de tests, GATeL permet de générer des séquences couvrant ces critères.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00680308 |
| Date | 09 January 2012 |
| Creators | Junke, Christophe |
| Publisher | Ecole Centrale Paris |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | fra |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds