Skip to Main content Skip to Navigation
Theses

Quasi optimal model checking for concurrent systems

Résumé : 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.
Mots-clés : Dépliage
Complete list of metadatas

https://tel.archives-ouvertes.fr/tel-02888087
Contributor : Abes Star :  Contact
Submitted on : Thursday, July 2, 2020 - 6:54:16 PM
Last modification on : Saturday, July 4, 2020 - 3:36:26 AM

File

edgalilee_th_2018_nguyen.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-02888087, version 2

Collections

Citation

Thi Thanh Huyen Nguyen. Quasi optimal model checking for concurrent systems. Data Structures and Algorithms [cs.DS]. Université Sorbonne Paris Cité, 2018. English. ⟨NNT : 2018USPCD087⟩. ⟨tel-02888087v2⟩

Share

Metrics

Record views

76

Files downloads

21