Cette thèse a eu pour but l'étude et la mise en oeuvre des méthodes de vérification par abstraction pour les modèles AltaRica. A cette effet, une méthode d'abstraction permettant l'utilisation d'une sous approximation de l'espace des états d'un système dans un algorithme CEGAR est présentée. Son utilisation permet d'accélérer l'algorithme CEGAR, ainsi que de réduire les ressources nécessaires lors de la vérification d'un modèle. Nous nous intéressons à une modélisation d'un sous ensemble du langage AltaRica , pour lequel une méthode d'abstraction hiérarchique est décrite, ainsi qu'un algorithme efficace permettant la vérification de contre-exemples issus de cette abstraction. La méthode proposée permet d'abstraire chaque composant de la hiérarchie indépendamment malgré la présence de priorités dans le modèle. Finalement l'implémentation de l'algorithme PCegar dans le model checker Mec 5 est présentée ainsi qu'une analyse de benchmarks sur des modèles académiques et un modèle industriel. / This thesis presents an abstraction verification method for AltaRica models. To this end a CEGAR algorithm that prunes away abstract states and therefore uses an underapproximation of the system state space is proposed. The use of an underapproximation of the abstract state space allow to accelerate the algorithm, and reduce the computational resources required by the algorithm. A CEGAR algorithm for a subset of the AltaRica language is also presented. A hierarchical abstractionscheme and an efficient counter-example analysis method are proposed. The abstraction scheme proposed allow to abstract each component independently despite the presence of priorities in the model. Finally, the implementation of our CEGAR with pruning method is present together with benchmarks on academic and industrial models.
| Identifer | oai:union.ndltd.org:theses.fr/2012BOR14641 |
| Date | 27 November 2012 |
| Creators | Chucri, Farès |
| Contributors | Bordeaux 1, Walukiewicz, Igor, Griffault, Alain, Sutre, Grégoire |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.008 seconds