Cette thèse porte sur l'aide à la construction de machines d'états UML de systèmes réactifs. Elle vise à définir un cadre théorique et pragmatique pour mettre en oeuvre une approche incrémentale caractérisée par une succession de phases de construction, évaluation et correction de modèles. Ce cadre offre des moyens de vérifier si un nouveau modèle est conforme à ceux définis durant les étapes précédentes sans avoir à demander une description explicite des propriétés à vérifier. Afin de pouvoir analyser les machines d'états, nous leur associons une sémantique LTS ce qui nous a conduit à définir une procédure de transformation automatique de machines d'états en LTS. Dans un premier temps, nous avons défini et implanté des techniques de vérification de relations de conformité de LTS (red, ext, conf, et confrestr). Dans un second temps, nous nous sommes intéressés à la définition d'un cadre de construction incrémentale dans lequel plusieurs stratégies de développement peuvent être mises en \oe uvre en s'assurant que le modèle final élaboré sera une implantation conforme à la spécification initiale. Ces stratégies reposent sur des combinaisons de raffinements qui peuvent être de deux types : le raffinement vertical pour éliminer l'indéterminisme et ajouter des détails ; le raffinement horizontal pour ajouter de nouvelles fonctionnalités sans ajouter d'indéterminisme. Enfin, nous transposons la problématique de construction incrémentale d'une machine d'états à la construction d'architectures dont les composants sont des machines d'états. Des conditions sont définies pour assurer la conformité entre des architectures dans le cas de la substitution de composants.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00527631 |
| Date | 01 October 2010 |
| Creators | Luong, Hong-Viet |
| Publisher | Université Paul Sabatier - Toulouse III |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds