| Titre : | Optimisation duModel Checker symbolique NuSMV (New Symbolic Model Verifier) Conception et implémentation des algorithmes de model checking en utilisant la librairie SDD (Sentential Decision Diagrams) | | Type de document : | projet fin études | | Auteurs : | Imad BOURIAN, Auteur | | Année de publication : | 2014 | | Langues : | Anglais (eng) | | Catégories : | Génie Logiciel
| | Mots-clĂ©s : | VĂ©rification formelle, Model Checking, Logique temporelle, Computation Tree Logic, Binary Decision Diagrams, Sentential Decision Diagrams | | Index. dĂ©cimale : | 1388/14 | | RĂ©sumĂ© : | Le présent rapport est une synthèse du travail effectué dans le cadre de mon projet de fin d’études au sein de l’équipe Spécification et Vérification de Systèmes (SVS) du Laboratoire d’Algorithmique, Complexité et Logique (LACL) de l’Université Paris-Est Créteil, pour l’obtention du titre d’ingénieur d’état en informatique.
Le sujet de stage porte sur la conception et l’implémentation des algorithmes de Model Checking CTL (Computation Tree Logic) en utilisant la librairie SDD (Sentential Decision Diagram). Ce travail s’inscrit dans le cadre du projet de recherche EQINOCS (Entropy and Quantity of Information in Computer Systems) déroulé au LACL en collaboration avec trois autres laboratoires d’informatique français (LIAFA, LIGM et VERIMAG). En effet, un des problèmes majeurs des solutions de Model Checking est l’explosion combinatoire de l’espace d’états modélisant le système à vérifier. Ce problème est traité dans les Model Checkers actuels en utilisant les diagrammes BDD (Binary Decision Diagrams) qui contribuent favorablement à la réduction des effets dus à ce problème. Cependant et étant donné la complexité des systèmes informatiques qui ne cesse d’accroitre, les approches basées sur ces diagrammes présentent toujours des limites. Ainsi, plusieurs travaux de recherche ont été menés dans l’objectif d’améliorer davantage le fonctionnement des Models Checkers.
Dans ce contexte, le laboratoire LACL m’a confié un projet dont l’objectif est d’apporter une solution plus efficace à la problématique de l’explosion combinatoire de l’espace d’états dans les Model Checkers. Ce projet consiste en la conception et l’implémentation des algorithmes de Model Checking CTL qui se basent sur la librairie SDD. Cette solution permet de vérifier si un système informatique modélisé sous forme d’un système d’états/transitions, satisfait une spécification donnée formulée à l’aide de la logique temporelle CTL.
L’approche proposée a été implémentée dans le Model Checker NUSMV (New Symbolic Model Verifier). Les résultats expérimentaux obtenus sont très satisfaisants.
|
Optimisation duModel Checker symbolique NuSMV (New Symbolic Model Verifier) Conception et implémentation des algorithmes de model checking en utilisant la librairie SDD (Sentential Decision Diagrams) [projet fin études] / Imad BOURIAN, Auteur . - 2014. Langues : Anglais ( eng) | Catégories : | Génie Logiciel
| | Mots-clĂ©s : | VĂ©rification formelle, Model Checking, Logique temporelle, Computation Tree Logic, Binary Decision Diagrams, Sentential Decision Diagrams | | Index. dĂ©cimale : | 1388/14 | | RĂ©sumĂ© : | Le présent rapport est une synthèse du travail effectué dans le cadre de mon projet de fin d’études au sein de l’équipe Spécification et Vérification de Systèmes (SVS) du Laboratoire d’Algorithmique, Complexité et Logique (LACL) de l’Université Paris-Est Créteil, pour l’obtention du titre d’ingénieur d’état en informatique.
Le sujet de stage porte sur la conception et l’implémentation des algorithmes de Model Checking CTL (Computation Tree Logic) en utilisant la librairie SDD (Sentential Decision Diagram). Ce travail s’inscrit dans le cadre du projet de recherche EQINOCS (Entropy and Quantity of Information in Computer Systems) déroulé au LACL en collaboration avec trois autres laboratoires d’informatique français (LIAFA, LIGM et VERIMAG). En effet, un des problèmes majeurs des solutions de Model Checking est l’explosion combinatoire de l’espace d’états modélisant le système à vérifier. Ce problème est traité dans les Model Checkers actuels en utilisant les diagrammes BDD (Binary Decision Diagrams) qui contribuent favorablement à la réduction des effets dus à ce problème. Cependant et étant donné la complexité des systèmes informatiques qui ne cesse d’accroitre, les approches basées sur ces diagrammes présentent toujours des limites. Ainsi, plusieurs travaux de recherche ont été menés dans l’objectif d’améliorer davantage le fonctionnement des Models Checkers.
Dans ce contexte, le laboratoire LACL m’a confié un projet dont l’objectif est d’apporter une solution plus efficace à la problématique de l’explosion combinatoire de l’espace d’états dans les Model Checkers. Ce projet consiste en la conception et l’implémentation des algorithmes de Model Checking CTL qui se basent sur la librairie SDD. Cette solution permet de vérifier si un système informatique modélisé sous forme d’un système d’états/transitions, satisfait une spécification donnée formulée à l’aide de la logique temporelle CTL.
L’approche proposée a été implémentée dans le Model Checker NUSMV (New Symbolic Model Verifier). Les résultats expérimentaux obtenus sont très satisfaisants.
|
|
138/99 
Faire une suggestion Affiner la recherche
Optimisation duModel Checker symbolique NuSMV (New Symbolic Model Verifier) Conception et implémentation des algorithmes de model checking en utilisant la librairie SDD (Sentential Decision Diagrams) / Imad BOURIAN
