Vers la vérification de propriétés de sûreté pour des systèmes infinis communicants : décidabilité et raffinement des abstractions

Abstract

La vérification de propriétés de sûreté des logiciels distribués basés sur des canaux fifo non bornés et fiables mène directement au model checking de systèmes infinis. Nous introduisons la famille des (q)ueueing (c)oncurrent (p)rocesses (QCP) composant des systèmes de transitions locaux, par exemple des automates finis/à pile, qui communiquent entre eux par des files fifo. Le problème d'atteignabilité des états de contrôle est indécidable pour des automates communicants et des automates à plusieurs piles, et par conséquent pour QCP.Nous présentons deux solutions pour contourner ce résultat négatif :Primo, une sur-approximation basée sur l'approche abstraire-tester-raffiner qui s'appuie sur notre nouveau concept de raffinement par chemin. Cette approche mène à permettre d'écrire un semi-algorithme du type CEGAR qui est implémenté avec des QDD et réalisé dans le framework McScM dont le banc d'essai conclut notre présentation.Secundo, nous proposons des restrictions pour les QCP à des piles locales pour démêler l'interaction causale entre les données locales (la pile), et la synchronisation globale. Nous montrons qu'en supposant qu'il existe une borne existentielle sur les exécutions et qu'en ajoutant une condition sur l'architecture, qui entrave la synchronisation de deux piles, on arrive à une réponse positive pour le problème de décidabilité de l'atteignabilité qui est EXPTime-complet (et qui généralise des résultats déjà connus). La construction de base repose sur une simulation du système par un automate à une pile équivalent du point de vue de l'atteignabilité --- sous-jacente, nos deux restrictions restreignent les exécutions à une forme hors-contexte. Nous montrons aussi que ces contraintes apparaissent souvent dans des situations ``concrètes''et qu'elles sont moins restrictives que celles actuellement connues. Une autre possibilité pour arriver à une solution pratiquement utilisable consiste à supposer une borne du problème de décidabilité : nous montrons que l'atteignabilité par un nombre borné de phases est décidable par un algorithme constructif qui est 2EXPTime-complet.Finalement, nous montrons qu'élargir les résultats positifs ci-dessus à la vérification de la logique linéaire temporelle demande soit de sacrifier l'expressivité de la logique soit d'ajouter des restrictions assez fortes aux QCP --- deux restrictions qui rendent cette approche inutilisable en pratique. En réutilisant notre argument de type ``hors-contexte'', nous représentons l'ordre partiel sous-jacent aux exécutions par des grammaires hypergraphes. Cela nous permet de bénéficier de résultats connus concertant le model checking des formules de la logique MSO sur les graphes (avec largeur arborescente bornée), et d'arriver aux premiers résultats concernant la vérification des propriétés sur l'ordre partiel des automates (à pile) communicants.