Return to search

Systèmes de transitions symboliques et hiérarchiques pour la conception et la validation de modèles B raffinés

Cette thèse propose une approche d'aide à la conception et au développement de modèles formels B. Cette approche se base sur la construction d'un système de transitions symboliques décrivant les comportements du modèle. Cette seconde vue est complémentaire avec la description orientée données du modèle B et peut être utilisée pour le décrire, le documenter ou le valider. Le système de transitions est élaboré à partir d'un espace d'états fourni par l'utilisateur et les transitions sont construites par résolution d'obligations de preuve. Nous proposons également de prendre en compte le processus de raffinement B en introduisant la notion de hiérarchie dans les systèmes de transitions. Cette représentation permet de mettre en évidence le lien entre les données des différents niveaux de raffinement. De plus, la méthode que nous proposons se base sur la décomposition des états d'une représentation du modèle abstrait, permettant ainsi de conserver la structure générale du système. Enfin, nous terminons ce manuscrit en décrivant l'outil GénéSyst qui implante cette méthode, ainsi que son utilisation dans le cadre du projet GECCOO, pour la vérification de propriétés de sécurité.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00216026
Date14 December 2007
CreatorsStouls, Nicolas
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0017 seconds