VÉRIFICATION DE SYSTÈMES CRITIQUES ASYNCHRONES PAR ABSTRACTION/RAFFINEMENT DE LA CONCURRENCE




Mots-clés : systèmes embarqués critiques, systèmes infinis, abstraction, raffinement, ordres partiels, dépliage.


Directeur : Igor Walukiewicz (CNRS DR)

Co-encadrants : Frédéric Herbreteau (MCF) et Grégoire Sutre (CNRS CR)

Sujet

Contexte

Les risques financiers, environnementaux et humains, et en conséquence les contraintes fixées par les normes et les organismes de certification imposent des démarches rigoureuses pour le développement des systèmes informatiques critiques. De ce fait, les méthodes formelles sont de plus en plus utilisées lors les cycles de développement. En témoigne le projet ANR SPACIFY1, dans lequel nous mettons au point avec nos partenaires un atelier de développement pour les logiciels embarqués de l'industrie spatiale.

Parmi les méthodes formelles, le model-checking consiste en la construction d'un modèle mathématique du système informatique et de sa spécification, puis en la preuve de la satisfaction ou de l'insatisfaction de cette dernière par le modèle. Celui-ci décrit les états du système et les changements d'états résultant des sollicitations extérieures. La spécification s'exprime le plus souvent en identifiant des états de défaillance. Les algorithmes de model-checking explorent alors le modèle afin de prouver l'inaccessibilité de ceux-ci.

Les états du système sont généralement définis par les valuations des variables de l'application, le plus souvent à valeurs dans des domaines infinis. Les algorithmes de model-checking sont donc confrontés à l'exploration de modèles infinis, sans qu'il n'y ait donc de garantie de terminaison (le problème étant indécidable). Parmi les solutions proposées à ce problème, l'abstraction consiste à plonger les domaines infinis des variables vers des domaines finis, par exemple via l'utilisation de prédicats. Un état du système n'est donc plus défini par la valeur des variables mais par celles de prédicats (par exemple $x\leq 3$) portant sur celles-ci. Cependant, à cause de la perte de précision engendrée, l'insatisfaction de la spécification par le modèle abstrait ne permet pas de conclure sur le modèle exact (par exemple pour la spécification $x\neq 3$ si le prédicat $x\leq 3$ est accessible). Le faux contre-exemple alors obtenu est utilisé par la phase de raffinement pour l'ajout de prédicats (par exemple, $x=3$) donnant lieu à un nouveau modèle abstrait. La méthode CEGAR2consiste alors en l'itération des phases d'abstraction/model-checking/raffinement. Lorsque le procédé se termine, il permet de prouver à moindre coût la satisfaction ou l'insatisfaction des spécifications par un système.

Cependant, même lorsque les modèles sont finis, on se heurte bien souvent à leur taille rédhibitoire. En particulier, dans le cadre du projet ANR SPACIFY, nous traitons des systèmes "Localement Synchrones, Globalement Asynchrones (GALS)" dont la taille des modèles croît exponentiellement avec le nombre de composants du système du fait de la concurrence entre eux (c'est le problème d'explosion combinatoire). Les algorithmes de model-checking classiques explorent en effet tous les entrelacements d'actions des différents composants autorisés par leurs interactions. Or beaucoup de ces entrelacements sont équivalents, par exemple lorsque deux actions sont permutées sans aucun effet sur l'atteignabilité des états de défaillance. Pour lutter contre ce problème, des techniques d'ordre-partiel ont été introduites. En particulier, la méthode de dépliage permet d'une part d'identifier automatiquement les entrelacements équivalents, et d'autre part de les représenter de façon compacte, par un ordre-partiel. La difficulté de cette approche réside dans le fait que le dépliage d'un système fini est infini. Il faut donc pouvoir en calculer une troncature finie qui préserve suffisamment d'information pour conclure sur le problème de vérification. Cette technique est notamment abondamment utilisée pour la vérification de réseaux de Petri bornés pour lesquels la troncature est aisée.

Problématique de la thèse

L'approche CEGAR a jusqu'ici été utilisée avec succès pour la vérification de programmes séquentiels. Pour les programmes concurrents, l'abstraction des données manipulées n'est plus suffisante en raison de l'explosion combinatoire du nombre d'entrelacements des actions des composants. Nous proposons donc deux axes d'extension de l'approche CEGAR aux relations de concurrence des systèmes afin d'obtenir des dépliages plus compacts.
  1. Vis-à-vis d'une certaine spécification, toutes les interactions (ou synchronisations) entre les composants du système ne sont pas nécessairement pertinentes. Elles visent, toutes ensembles, à satisfaire l'ensemble des spécifications, mais lorsqu'on considère celles-ci individuellement, seules quelques interactions servent à les garantir. Nous espérons donc pouvoir abstraire certaines synchronisations, afin d'obtenir une troncature plus compacte du fait que la concurrence augmente dans le modèle abstrait. Bien entendu, le choix de l'abstraction n'est pas anodin pour parvenir à une preuve de satisfaction ou d'insatisfaction des spécifications. De plus il n'est pas possible de le connaître a priori.

  2. La technique de dépliage est d'autant plus efficace que les modèles sont concurrents. Par ailleurs, l'utilisation de modèles d'ordre partiel repose sur des algorithmes génériques pour les calculer depuis des modèles usuels (par exemple, des systèmes de transitions). Ces calculs sont cependant coûteux, donc uniquement applicable pour de petits composants. Nous proposons une approche CEGAR basée sur la construction de modèles d'ordre partiel abstraits. Le principe est de supposer une forte concurrence entre les actions des modèles de chaque composant, puis de les raffiner suivant les faux contre-exemples trouvés par la procédure de model-checking (en faisant tendre les ordres partiels de ces modèles vers des ordres totaux).

Ces deux approches sont complémentaires entre elles et complémentaires de l'abstraction plus usuelle des données du système. En effet, d'une part l'abstraction des données crée un contexte favorable à l'abstraction de la concurrence. D'autre part, en n'abstrayant que les données, les modèles obtenus sont encore gros (et donc difficiles à vérifier) car ils codent précisément les séquences d'instructions du système. L'abstraction de ces séquences est donc une technique prometteuse pour le passage à l'échelle de la vérification des programmes concurrents.

Le travail de thèse comprend d'une part la définition des abstractions et des raffinements pour les deux axes présentés ci-dessus, et d'autre part l'implantation de deux techniques dans l'outil ESU3. Ce travail s'inscrit en prolongement de la thèse de Tran The Quang, et vise à automatiser la modélisation par ordre partiel et à rendre l'étape de model-checking par dépliage plus performante. Enfin, le projet SPACIFY fournit un cadre idéal d'expérimentation et de confrontation aux besoins industriels pour les systèmes embarqués critiques.

Bibliographie

Bibliographie

1
P. A. Abdulla, S. P. Iyer, and A. Nylén.
Unfoldings of unbounded petri nets.
In Proc. of 12th Int. Conf. on Computer Aided Verification (CAV'00), volume 1855 of Lecture Notes in Computer Science, pages 495-507. Springer, 2000.

2
T. Ball and S. K. Rajamani.
Automatically validating temporal safety properties of interfaces.
In Proc. 8th Int. SPIN Workshop (SPIN'2001), Toronto, Canada, May 2001, volume 2057 of Lecture Notes in Computer Science, pages 103-122. Springer, 2001.

3
S. Chaki, E. M. Clarke, N. Kidd, T. W. Reps, and T. Touili.
Verifying concurrent message-passing c programs with recursive calls.
In Proc. 12th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), Vienna, Austria, Mar.-Apr. 2006, volume 4144 of Lecture Notes in Computer Science, pages 334-349. Springer, 2006.

4
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith.
Counterexample-guided abstraction refinement.
In Proc. 12th Int. Conf. Computer Aided Verification (CAV'2000), Chicago, IL, USA, July 2000, volume 1855 of Lecture Notes in Computer Science, pages 154-169. Springer, 2000.

5
J. Desel, G. Juhás, and C. Neumair.
Finite unfoldings of unbounded petri nets.
In Proc. 25th Int. Conf. on Applications and Theory of Petri Nets (ICATPN'04), volume 3099 of Lecture Notes in Computer Science, pages 157-176. Springer, 2004.

6
J. Esparza and S. Römer.
An unfolding algorithm for synchronous products of transition systems.
In 10th Int. Conf. on Concurrency Theory (CONCUR'99), volume 1664 of Lecture Notes in Computer Science, pages 2-20. Springer, 1999.

7
J. Esparza, S. Römer, and W. Vogler.
An improvement of McMillan's unfolding algorithm.
Formal Methods in System Design, 20(3):285-310, 2002.

8
S. Graf and H. Saïdi.
Construction of abstract state graphs with PVS.
In Proc. 9th Int. Conf. Computer Aided Verification (CAV'97), Haifa, Israel, June 1997, volume 1254 of Lecture Notes in Computer Science, pages 72-83. Springer, 1997.

9
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre.
Lazy abstraction.
In Proc. 29th ACM Symp. Principles of Programming Languages (POPL'2002), Portland, OR, USA, Jan. 2002, pages 58-70. ACM Press, 2002.

10
F. Herbreteau, G. Sutre, and Q.T. Tran.
Unfolding concurrent well-structured transition systems.
In Proc. of the 13th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), Lecture Notes in Computer Science, Braga, Portugal, mar-apr 2007. Springer.

11
K. L. McMillan.
A technique of state space search based on unfolding.
Formal Methods in System Design, 6(1):45-45, 1995.

12
K. L. McMillan.
Lazy abstraction with interpolants.
In Proc. 18th Int. Conf. Computer Aided Verification (CAV'06), Seattle, WA, USA, Aug. 2006, volume 4144 of Lecture Notes in Computer Science, pages 123-136. Springer, 2006.

À propos de ce document...

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 -nonavigation cegar_unfolding.tex

The translation was initiated by Frédéric Herbreteau on 2007-01-15


Notes

... SPACIFY1
"Ingénierie des modèles et méthodes formelles intégrées pour le développement des logiciels de vol spatiaux".
... CEGAR2
Counter-Example Guided Abstraction Refinement.
...Esu3
"Event Structure Unfolder" développé par Tran The Quang.


Frédéric Herbreteau 2007-01-15