Ce travail s'inscrit dans le cadre des méthodes formelles et des outils pour la spécification, la programmation, la vérification et la validation des logiciels réactifs à l'aide du langage synchrone Lustre. Nous avons étendu l'environnement de développement actuel de ces logiciels en lui adjoignant des outils de validation de spécifications et de test de programmes. Nous proposons une technique de construction automatique d'un simulateur aléatoire de l'environnement externe du logiciel ainsi que d'un simulateur des comportements sûrs de ce dernier. Exécutés conjointement, ces deux simulateurs permettent, par observation, la validation des spécifications de l'environnement et des propriétés de sûreté. La simulation de l'environnement constitue également un moyen de test aléatoire du logiciel. Une variante de cette technique est le test des propriétés de sûreté. Ce type de test favorise l'exécution des comportements de l'environnement du logiciel qui peuvent mettre en évidence avec une plus grande probabilité des violations des propriétés de sûreté. Enfin, nous définissons des critères de couverture pour le test structurel en s'appuyant sur le réseau d'opérateurs associé à un programme Lustre. Les conditions d'exécution des composants du réseau satisfaisant les critères sont calculées automatiquement ce qui permet la génération automatique de données de test ainsi que la mesure du taux de couverture obtenu. Toutes ces techniques sont formellement définies. Une illustration de leur application sur un exemple de logiciel synchrone que nous avons développé à cet effet complète notre étude.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00005010 |
| Date | 30 September 1996 |
| Creators | Parissis, Ioannis |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0017 seconds