Trois approches pour la modélisation et la vérification de systèmes embarqués
L’objectif de cet article est de montrer la faisabilité de la vérification formelle de
propriétés mixtes fonctionnelles et temps réel sur un système embarqué. Trois approches sont
développées. Une première comparaison oppose d’une part une technique opérant sur un
modèle de temps continu (le vérifieur UPPAAL associé aux automates temporisés) à des
techniques opérant sur des modèles de temps discrets. Parmi ces dernières, une seconde
comparaison oppose les techniques de « model checking », illustrées ici par le vérifieur SMV
associé au langage LUSTRE, à des techniques plus couramment utilisées dans le domaine de
l’optimisation combinatoire, illustrées dans cet article par une méthode de satisfaction de
contraintes. Ces comparaisons, réalisées sur un exemple du monde avionique, contribuent à
montrer la robustesse des approches par contraintes face au phénomène de l’explosion
combinatoire.
The aim of this article is to establish the formal verification feasibility of mixed
functional and real time properties in the context of embedded systems. Three different
approaches are compared. A first experiment compares a verification technique based on a
continuous time model (the UPPAAL model checker associated with the timed automata
formalism) to techniques based on a discrete time model. Among these last techniques, a
second experiment compares a model checking technique (the model checker SMV associated
with the synchronous language LUSTRE) to a constraint satisfaction method usually used in
the context of combinatorial optimisation. These comparisons lead to the conclusion that the
constraint satisfaction methods seem to be more robust, when increasing the complexity of
the system to verify, than the other techniques.
F.BONIOL, G.BEL, J.ERMONT
Reçu le 1 juillet 2002.
Accepté le 17 février 2003.
vérification, systèmes embarqués, temps réel, automates temporisés, langage synchrone, satisfaction de contraintes.
verification, embedded systems, real time, timed automata, synchronous language, constraint satisfaction problem.
Français
|
