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)
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
) 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
si le prédicat
est accessible). Le faux contre-exemple alors obtenu est utilisé par
la phase de raffinement pour l'ajout de prédicats (par exemple,
)
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.
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.
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