ACCUEIL

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

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 31/3 - 2012  - pp.337-373  - doi:10.3166/tsi.31.337-373
TITRE
Vérification partielle de programmes de contrôle-commande par interprétation abstraite

TITLE
Abstract interpretation based partial verification of control-command programs

RÉSUMÉ

L’analyse statique par interprétation abstraite cherche à sur-approximer l’ensemble des comportements possibles des programmes pour s’assurer de l’absence de certains types de bogues. Dans le cas des programmes de contrôle-commande, le comportement du programme dépend de l’environnement extérieur avec lequel il interagit. Prendre en compte cet environnement, souvent largement sur-approximé dans les analyseurs, permet de prouver de nouvelles propriétés concernant le programme de contrôle-commande. Dans cet article, nous nous intéressons à une classe de programme de contrôle-commande pour laquelle une description de l’environnement physique existe sous forme d’équations différentielles. Nous décrivons de nouvelles méthodes d’analyse de ces systèmes qui sur-approximent l’ensemble des trajectoires possibles pour l’environnement continu, permettant ainsi de prouver, dans certains cas, des propriétés de sûreté sur l’algorithme de contrôle-commande.



ABSTRACT

In the field of static analysis, abstract interpretation based techniques compute over approximations of the set of possible behaviors of programs. These over-approximations give properties on the program that can be used to prove the abscence of some bugs. In the case of control command programs, the behavior of the program depends on the physical environment with which it interacts. This environment is often largely over-approximated in classical analyzers, taking it into account can lead to proving new properties conerning the controlcommand program. In this article, we consider a class of control-command programs for which a description of the physical environment is given as a set of differential equations. We present new analysis methods that over-approximate the set of possible trajectories for the continuous environment. This allows to prove, in some cases, safety properties on the control-command algorithm.



AUTEUR(S)
Olivier BOUISSOU

MOTS-CLÉS
analyse statique, interprétation abstraite, systèmes hybrides, contrôle commande

KEYWORDS
static analysis, abstract interpretation, hybrid systems, control-command.

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é par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (913 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier