Dans cette thèse nous nous intéressons à la vérification formelle de système critique par la technique du model-checking. Plus précisément, nous nous situons dans le contexte de la vérification des systèmes temporisés, où la correction du système dépend du respect des contraintes temporelles.
Ces travaux de thèse sont structurés en deux parties.
La première partie étudie la modélisation et la vérification formelle par model-checking de systèmes temps réels critiques dans un contexte industriel.
Dans un premier temps, nous présentons des exemples d'utilisation opérationnelle de techniques formelles dans l'industrie aéronautique et spatiale. Puis nous proposons une formalisation d'une fonction de capture d'altitude d'un système de pilote automatique dans une architecture de type command/monitoring contrainte par des exigences de sûreté de fonctionnement. Le modèle est décrit à l'aide du langage FIACRE et la vérification des contraintes temporelles par model-checking est réalisée avec l'outil TINA.
La deuxième partie s’intéresse aux problèmes fondamentaux du model-checking. Une difficulté inhérente au model-checking est l'explosion combinatoire. De nombreuses techniques permettent d'en limiter l'impact ; parmi celles-ci on trouve la réduction par symétrie. Cette approche utilise les symétries structurelles d'un système pour définir une relation d'équivalence sur ses états. De nombreux travaux exploitant les symétries existent pour le model-check ing non temporisé.
Dans un contexte temporisé, une difficulté supplémentaire tient au fait que l'espace d'états est généralement infini. Pour le model-checking temporisé, on aura recours à des abstractions finies de leurs espaces d'états infinis. L'abstraction des classes d'états est l'une de ces abstractions, applicable aux réseaux de Petri temporels (TPN). Des techniques efficaces dans un contexte atemporel ne le sont pas nécessairement dans un contexte temporisé. L'exploitation des symétrie dans le contexte temporisé est plus récente. Des travaux ont été réalisés dans le contexte des automates temporisés, mais aucun résultat n'était encore disponible dans le contexte des TPN. La contribution principale de cette thèse est donc une méthode d'exploitation des symétries pour les TPN.
Deux problèmes sont à résoudre : calculer les symétries d'un système, puis exploiter ces symétries pour réduire le nombre d'états à explorer lors du model-checking.
Nous calculons les symétries par une approche combinatoire. Nous proposons un langage de composition de réseaux qui, étant donné un groupe de permutations, permet la construction d'un réseau symétrique et d'un sous-groupe de ses automorphismes isomorphe au groupe donné. Cette solution s'applique quelque soit le groupe de permutations ou les synchronisations.
Les réductions d'espaces d'états exploitent la relation d'équivalence induite par les symétries. Malheureusement, décider si deux états sont équivalents est aussi complexe que le problème de l'isomorphisme de graphe, ce qui rend toute implémentation naïve impraticable. Des travaux antérieurs aux nôtres, dans le contexte atemporel, ont montré que des solutions polynomiales en le nombre de composants sont applicables à certaines classes de réseaux symétriques.
Nous étendons cette approche aux TPN, en proposant des méthodes de réduction efficaces là où elles sont applicables et détectons les cas moins favorables. Notre méthode repose sur la définition d'un ordre total entre les classes d'états équivalentes par la relation de symétrie. Cet ordre total permet le calcul efficace des représentants canoniques des classes d'équivalence.
Finalement, nous présentons une implémentation de la méthode dans l'outil TINA, pour le cas où des représentants canoniques peuvent être calculés efficacement. Les résultats expérimentaux sont très encourageants. |
In this thesis we focus on formal verification of critical systems by model-checking techniques. Specifically, the context of this work is the verification of timed systems, where correction of the system depends on meeting some timing constraints.
This thesis work is structured in two parts. The first studies the modeling and formal verification by model-checking of critical real-time systems in an industrial context.
First, we present examples of operational use of formal techniques in aerospace applications. Then we propose a formalization of a function of altitude capture of an autopilot system in a command/ monitoring architecture constrained by safety requirements. The model is described using the language FIACRE; verification of the timing constraints by model-checking is performed with the TINA tool.
The second part deals with some fundamental problems of model checking. An inherent difficulty in model-checking is the combinatorial explosion. Many techniques are used to limit their impact; among which is reduction by symmetry. This approach uses the structural symmetry of a system for defining an equivalence relation on its states. Many works exploiting symmetries exist for untimed model-checking.
In a timed context, an additional difficulty is that the state space is generally infinite. For model-checking, we have to use finite abstractions of their infinite state spaces. The state classes abstraction is one of these abstractions, applicable to Time Petri nets (TPN). Techiques which are effective in untimed contexts are not necessarily in timed environments. The exploitation of symmetry in timed contexts is more recent. Some works are available for Timed Automata, but no results were yet available in the context of TPN. The main contribution of this thesis is a symmetry reduction method for TPN.
Two problems have to be solved: calculate the symmetries of the system and then use these symmetries to reduce the number of states to explore during model-checking.
We calculate the symmetries with a combinatorial approach. We offer a composition language for TPN that, given a group of permutations, allows the construction of a symmetrical net and a sub-group of its automorphisms isomorphic to the given group. This solution applies whatever the permutation group or synchronizations.
Reduction of state spaces exploits the equivalence relation induced by symmetries. Unfortunately, deciding whether two states are equivalent is as complex as the problem of graph isomorphism, which makes any naive implementation impractical. Previous work in untimed contexts showed that polynomial solutions in the number of components can be found for certain classes of symmetrical nets.
We extend this approach to TPN, proposing effective symmetry reduction methods when possible and detect the least favorable cases. Our method relies on a total order between the state classes equivalent by symmetry. This total order allows an efficient computation of canonical representatives of symbolic states..
Finally, we present an implementation of the method in the TINA tool for the case where canonical representatives can be efficiently computed. The experimental results are very encouraging.
|