Les logiciels sont désormais un des composants essentiels des équipements modernes. Ils sont responsables de leur sûreté et fiabilité. Par sûreté, nous entendons que le système garantit que ''rien de dangereux n'arrive jamais''. Ce type de propriété peut se réduire à un problème d'accessibilité: pour démontrer la propriété il suffit de démontrer qu'un ensemble d'états ''dangereux'' ne sont pas atteignables. Ceci est particulièrement important pour les systèmes critiques: les systèmes dont une défaillance peut mettre en jeu des vies humaines ou l'économie d'une entreprise. Afin de garantir un niveau de confiance suffisant dans nos équipements modernes, un grand nombre de méthodes de vérification ont étaient proposées. Ici nous nous intéressons au model checking: une méthode formelle de vérification de système. L'utilisation de méthodes de model checking et de model checker permet d'améliorer les analyses de sécurité des systèmes critiques, car elles permettent de garantir l'absence de bug vis-à-vis des propriétés spécifiées. De plus, le model checking est une méthode automatique, ceci permet à des utilisateurs non-spécialistes d'utiliser ces outils. Ceci permet l'utilisation de cette méthode à une grande communauté d'utilisateur dans différents contextes industriels. Mais le problème de l'explosion combinatoire de l'espace des états reste une difficulté qui limite l'utilisation de cette méthode dans un contexte industriel. Nous présentons deux méthodes de vérification de modèle AltaRica. La première méthode présente un algorithme CEGAR qui élague des états de l'abstraction, ce qui permet d'utiliser une sous-approximation de l'espace des états d'un système. Grâce à l'utilisation de cette sous-approximation, nous pouvons détecter des contre-exemples simples, utiliser des méthodes de réduction pour éliminer des états abstraits, ce qui nous permet de minimiser le coût de l'analyse des contre-exemples, et guider l'exploration de l'abstraction vers des contre-exemples qui sont plus pertinents. Nous avons développé cet algorithme dans le model checker Mec 5, et les expérimentations réalisées ont confirmé les améliorations attendues.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-01011163 |
| Date | 27 November 2012 |
| Creators | Chucri, Farès |
| Publisher | Université Sciences et Technologies - Bordeaux I |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0024 seconds