LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Actualité » Doctorants

COLANGE Maximilien

Docteur
Équipe : MoVe
Date de départ : 19/12/2013
https://www.lrde.epita.fr/~max/
Direction de recherche : Fabrice KORDON
Co-encadrement : BAARIR Souheib, THIERRY-MIEG Yann

Exploitation des symétries pour le modèle checking : du modèle au codage

Les systèmes répartis deviennent omniprésents au quotidien, en particulier dans des domaines critiques, requérant une forte garantie de fiabilité. Les approches basées sur le test sont intrinsèquement non-exhaustives, rendant nécessaire l’usage de méthodes formelles. Parmi elles, nous nous concentrons sur le model-checking, qui explore tous les comportements d’un système pour s’assurer que sa spécification est respectée. Mais cette approche se heurte à l’explosion combinatoire : le nombre d’états d’un système réparti croît exponentiellement avec son nombre de composants.
Nous retenons deux des nombreuses solutions à ce problème : - les symétries pour identifier des comportements similaires : ils partagent des propriétés communes, ce qui réduit le nombre d’états à explorer. - des structures de données compactes, comme les diagrammes de décision (DD), pour réduire l’empreinte mémoire de l’exploration.
Nous proposons trois principales contributions : - La réduction par symétries et les DD sont théoriquement orthogonaux, mais se combinent mal en pratique, car l’efficacité des DD repose sur l’emploi d’algorithmes dédiés. Nous proposons un nouvel algorithme pour appliquer la réduction par symétries sur des DD, et démontrons son efficacité pratique. - Classiquement, les opérations sur les DD sont encodées après un pré-calcul de toutes les entrées possibles. Nous offrons un nouveau mécanisme de manipulation des DD, entièrement symbolique, qui évite un tel pré-calcul. Nous démontrons son efficacité pour encoder une relation de transition. Nous montrons comment ces deux contributions peuvent être appliquées à un formalisme déjà existant, les Symmetric Nets with Bags.
Soutenance : 10/12/2013 - 14h - Site Jussieu 25-26/105
Membres du jury :
Pr. Ahmed Bouajjani [rapporteur] (Université Paris Diderot)
Pr. François Vernadat [rapporteur] (INSA Toulouse)
Dr. Souheib Baarir (Université Paris Ouest Nanterre la Défense)
Pr. Béatrice Bérard (Université Pierre et Marie Curie)
Pr.Dr.-Ing. Monika Heiner (Brandenburg University of Technology Cottbus)
Dr. Tommi Junttila (Aalto University)
Pr. Fabrice Kordon (Université Pierre et Marie Curie)
Dr. Yann Thierry-Mieg (Université Pierre et Marie Curie)

Publications 2011-2018

 Mentions légales
Carte du site |