Description
Date depot: 1 janvier 1900
Titre: Model checking adapté aux spécifications et propriétés à vérifier
Directeur de thèse:
Fabrice KORDON (LIP6)
Directeur de thèse:
Alexandre DURET-LUTZ (LRE)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
{{Contexte et motivation}}
Le model checking est un ensemble de techniques permettant de vérifier
formellement un système. Par système nous entendons par exemple un
circuit électronique ou bien un protocole de communication entre un
client et un serveur. À partir d'un modèle du système, et d'une
spécification des propriétés attendues, on réalise une série
d'opérations entièrement automatiques afin de déterminer si le modèle
du système vérifie bien les propriétés dans toutes les exécutions
possibles.
Plusieurs approches existent selon les types de modèles et de
spécifications utilisés. Par exemple l'approche automate du model
checking permet de vérifier des propriété exprimées par des formules
de logique temporelle à temps linéaire (du style 'si un client envoie
une demande infiniment souvent, alors il obtiendra une réponse du
serveur infiniment souvent') sur des modèles représentables par des
automates finis. D'autres approches s'appuient sur des formalismes
différents. Par exemple des techniques de model checking symboliques
permettent de vérifier des propriétés exprimées avec un logique à
temps arborescent sur des modèles représentés à l'aide de diagrammes
de décisions.
Chacune de ces méthodes peut bien sûr être déclinée de multiple façons
en variant les algorithmes mis en oeuvre. La construction d'un outil
de model checking aujourd'hui demande obligatoirement de faire des
choix. Le choix des formalismes utilisés pour représenter modèles et
propriétés, le choix des algorithmes utilisés pour effectuer la
vérification en elle-même, le choix des structures de données utilisés
par ces algorithmes, etc. À cause de ces choix, un model checker
donné sera utilisé pour résoudre une certaine classe de problèmes sur
laquelle on sait qu'il est efficace. Une personne possédant un modèle
et des propriétés à vérifier devra choisir le meilleur outil pour
répondre à son problème, ou bien modifier son problème pour le traiter
avec l'outil dont elle dispose.
{{Objectif proposé}}
Nous aimerions unifier et modulariser les différentes approches
existantes au sein d'un même framework. Ce framework permettrait, en
fonction du modèle et des propriété à y vérifier, de faire les choix
(peut-être automatiquement) des différents paramètres et algorithmes,
afin de construire la chaîne de model checking idéale.
Doctorant.e: Ben Salem Ala Eddine