ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne

APPEL À
CONTRIBUTION

Automates cellulaires et réseaux d automates

En savoir plus >>
Autres revues >>
Technique et Science Informatiques
0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 22/5 - 2003  - pp.539-569  - doi:10.3166/tsi.22.539-569
TITRE
Trois approches pour la modélisation et la vérification de systèmes embarqués

RÉSUMÉ
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.

ABSTRACT
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.

AUTEUR(S)
F.BONIOL, G.BEL, J.ERMONT

Reçu le 1 juillet 2002.    Accepté le 17 février 2003.

MOTS-CLÉS
vérification, systèmes embarqués, temps réel, automates temporisés, langage synchrone, satisfaction de contraintes.

KEYWORDS
verification, embedded systems, real time, timed automata, synchronous language, constraint satisfaction problem.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé 
   
ACCÉDER A L'ARTICLE COMPLET  (354 Ko)
--> NÉCESSITE ADOBE DIGITAL EDITIONS :



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
made by WAW Lavoisier