Quasi optimal model checking for concurrent systems
Vérification de modèle quasi-optimale de systèmes concurrents
Résumé
By exhaustively exploring all possible behaviours of the system, model checking has to face the state space explosion problem. We target the verification of concurrent programs. Dynamic partial-order reduction (DPOR), is a mature approach to mitigate the state explosion problem based on Mazurkiewicz trace theory, whereas unfolding is still at an initial state for targetting programs. We propose to combine DPOR and unfolding into an algorithm called Unfolding based POR. In order to obtain optimality, the algorithm is forced to compute sequences of transitions known as alternatives. In this thesis, we prove that computing alternatives in optimal DPOR is an NP-complete problem. As a trade-off solution, we propose a hybrid approach called Quasi-Optimal POR (QPOR). In particular, we provide a new notion of k-partial alternative and a polynomial algorithm to compute alternative executions. Another main algorithmic contribution is to represent causality and conflict as a set of trees where events are encoded as one or two nodes in two different trees. We show that checking causality and conflict between events amounts to an efficient traversal in one of these trees. We also implement the algorithm and data structures in a new tool. Besides the algorithmic improvements guaranteed by QPOR, parallelization is another way to speed up the unfolding exploration, thus we propose a parallel algorithm based on parallelizing QPOR. Finally, we conduct experiments on the sequential implementation of QPOR and compare the results with other state-of-art testing and verification tools to evaluate the efficiency of our algorithms. The analysis shows that our tool outperforms them.
En effectuant une exploration exhaustive de tous les comportements possibles du système, le model checking fait face au problème de l’explosion de cet espace d’états. Notre but est de vérifier des programmes concurrents. Nous avons proposé de combiner la DPOR et le dépliage dans un algorithme appelé POR basée sur le dépliage. Dans cette thèse, nous prouvons que le calcul des alternatives dans une DPOR optimale est un problème NP-complet. Nous proposons une approche hybride appelée réduction d’ordre partiel quasi-optimale (QPOR). En particulier, nous proposons une nouvelle notion d’alternative k-partielle et un algorithme en temps polynomial. Une autre contribution algorithmique de cette thèse est la représentation des relations de causalité et de conflit dans le dépliage comme un ensemble d’arbres dans lequel les événements sont encodés comme un ou deux nœuds dans deux arbres différents. Nous montrons que vérifier la causalité et le conflit entre deux événements revient à une traversée efficace d’un des deux arbres. Nous détaillons l’implémentation de l’algorithme et les structures de données utilisées dans un nouvel outil. Outre les améliorations algorithmiques garanties par QPOR, la parallélisation est un autre moyen d’accélérer l’exploration. Par conséquent, nous proposons un algorithme de QPOR parallèle. Enfin, nous présentons des expériences sur l’implémentation séquentielle de QPOR et comparons les résultats avec d’autres outils de test et de vérification afin d’évaluer l’efficacité de nos algorithmes. L’analyse des résultats montre que notre outil présente de meilleures performances que ceux-ci.
Origine : Fichiers produits par l'(les) auteur(s)