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 33/1-2 - 2014  - pp.159-162
TITRE
Analyse statique de programmes et systèmes numériques

RÉSUMÉ

Alors que la complexité des traitements informatiques dans les systèmes embarqués croit chaque jour, la sûreté du fonctionnement de ces systèmes devient un enjeu crucial, tout particulièrement pour les systèmes critiques. Plus largement, synthétiser et garantir des propriétés sur le comportement d’un programme, est un objectif naturel et de large utilité. Cette habilitation (Putot, 2012) porte sur la validation automatique de propriétés numériques des programmes, par des méthodes d’analyse statique par interprétation abstraite (Cousot, Cousot, 1977). Une première partie du document porte sur une classe de domaines abstraits zonotopiques (Goubault, Putot, 2006 ; 2008 ; 2009 ; Ghorbal et al., 2009 ; 2010 ; Goubault, Putot, Vedrine, 2012 ; Goubault, Gall, Putot, 2012), faiblement relationnels et peu coûteux. Ces domaines sont basés sur l’arithmétique affine (Comba, Stolfi, 1993), une extension de l’arithmétique d’intervalles tirant parti des corrélations linéaires entre variables, dont un des avantages est de permettre une linéarisation facile et rapide des expressions non linéaires. Si l’abstraction des expressions arithmétiques est naturelle par extension directe de l’arithmétique affine, une des difficultés spécifique à l’interprétation abstraite est la définition d’opérateurs d’union d’états (Goubault, Putot, 2008 ; 2009 ; Goubault, Gall, Putot, 2012) et d’intersection d’un état par une garde (Ghorbal et al., 2010). Dans le chapitre dédié aux applications, nous montrons que ces domaines zonotopiques permettent un calcul précis d’invariants pour de larges classes de programmes. Ils présentent aussi la particularité d’exprimer des abstractions fonctionnelles, c’est-à-dire d’exprimer les valeurs des variables comme des fonctions des entrées et paramètres incertains du programme. Nous pouvons ainsi prouver des propriétés fonctionnelles des programmes, et par exemple borner l’erreur de méthode d’un algorithme ou vérifier, de façon exacte ou approchée, des identités remarquables. Nous pouvons également tirer parti de cette abstraction fonctionnelle pour utiliser ces abstractions de façon modulaire (Goubault, Putot, Vedrine, 2012).



AUTEUR(S)
Sylvie PUTOT

LANGUE DE L'ARTICLE
Français

 PRIX
GRATUIT
   
ACCÉDER A L'ARTICLE COMPLET  (55 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier