ACCUEIL

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

APPEL À
CONTRIBUTION

Le comité de rédaction du JESA lance un appel à proposition de numéros spéciaux.

En savoir plus >>
Autres revues >>

Journal Européen des Systèmes Automatisés

1269-6935
Revues des Systèmes
 

 ARTICLE VOL 47/1-3 - 2013  - pp.61-75  - doi:10.3166/jesa.47.61-75
TITRE
Vérifier le comportement du code d’un système embarqué à partir de son modèle

RÉSUMÉ
Afin de réduire les coûts induits par la vérification, les méthodes formelles, telles que l’analyse statique, permettent de prouver automatiquement des propriétés sur du code. Malheureusement, ces techniques sont difficiles à appréhender et à mettre en pratique par des non-spécialistes. Le but des travaux présentés dans cet article est de faire le lien entre la spécification basée modèle et l’implémentation d’un système réactif embarqué. Nous proposons de générer automatiquement sur le code source les annotations de preuve correspondant aux propriétés comportementales d’un système, et ce, à partir de son modèle de conception. Ces propriétés peuvent ensuite être vérifiées par des outils d’analyse statique, afin de s’assurer que le comportement du code est conforme au modèle. Nous présentons ici, un sous-ensemble des machines à états UML, pour modéliser le système, pour lequel nous donnerons une sémantique formelle, notre méthode de génération d’annotations ainsi que son implémentation.


ABSTRACT
To reduce the costs of verification, formal methods, such as static analysis, allow to automatically prove code properties. Unfortunately, these techniques are difficult to understand and to use by non-specialists. The aim of this paper is to make the link between model based design and the code implementation of a reactive embedded system. We propose to generate automatically code annotations corresponding to the behavioural properties of a system. These properties are derived from the design model and they can be verified by static analysis tools. In this paper, we present a subset of UML state machine to model systems, we give a formal semantics of this subset and the method for annotations generation.


AUTEUR(S)
Anthony FERNANDES PIRES, Thomas POLACSEK, Virginie WIELS, Stéphane DUPRAT

MOTS-CLÉS
vérification, UML, méthodes formelles, ingénierie dirigée par les modèles.

KEYWORDS
verification, UML, formal methods, model-driven engineering.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (277 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier