A partir de cette page vous pouvez :
Retourner au premier Ă©cran avec les Ă©tagĂšres virtuelles... |
RĂ©sultat de la recherche
1 rĂ©sultat(s) recherche sur le mot-clĂ© 'Vérification formelle, Model Checking, Logique temporelle, Computation Tree Logic, Binary Decision Diagrams, Sentential Decision Diagrams'
Affiner la recherche Faire une suggestion
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
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.
RĂ©servation
RĂ©server ce document
Exemplaires
Code barre Cote Support Localisation Section DisponibilitĂ© 1388/14 1388/14 IMA Texte imprimé unité des PFE PFE/2014 Disponible