Vérification et Validation Formelle
de Programmes
YESLI Yasmine
Université Mouloud Mammeri de Tizi-Ouzou
2018/2019
Programme
Introduction
Systèmes de transitions
Logique temporelle : Linéaire et Arborescente
Modèle Checking
Arbre Binaire de Décision
2
Introduction
Historiquement, pour vérifier ou valider un programme, on
faisait appel à deux méthodes :
1- Tests ( Jeux d’essais ) : qui se font directement sur le
programme.
2- Simulation : qui se fait sur un modèle théorique avant la
réalisation du système.
3
Introduction
Quels sont les inconvénients de ces deux méthodes ?
1- Il est souvent très couteux de corriger les erreurs ( tester ou
simuler un avion par exemple) ;
2- On n’est pas sûr d’avoir effectué tous les tests d’une manière
exhaustive (dans le cas d’un jeu d’essais).
3- On n’est pas sûr d’avoir envisagé toutes les études de cas
possibles d’une manière exhaustive ( dans le cas de la
simulation).
Nécessité d’utiliser des méthodes plus sûres : c’est les
méthodes formelles.
4
Introduction
Pourquoi vérifier ?
1- Besoin de s’assurer de la fiabilité et de la sureté des
programme, c.à.d.
que les programmes répondent aux attentes des utilisateurs
et fonctionnent sans erreurs.
2- L’erreur est interdite dans certains systèmes dit critiques.
5
Introduction
Qu’est ce qu’un système critique ?
Les systèmes critiques ont pour objectif le contrôle d’un
processus qui communique avec son environnement par
l’intermédiaire de capteurs, thérmomètres, signaux, claviers, etc.
Comme le cas de l’aéronautiques , de la téléchirurgie, du
payement par carte à puce , du contrôle d’une centrale nucléaire,
..etc. ,
Ces systèmes n’ont pas pour but de calculer un résultat, mais
d’assurer le fonctionnement permanent du processus contrôlé :
d’où le nom de systèmes réactifs.
Ces systèmes sont souvent temps réels et distribués.
6
Introduction
7
Introduction
Exemples de systèmes critiques :
Pacemaker Pilote automatique
8
Introduction
L’absence de vérification, ou une vérification mal utilisée peut
entrainer de graves conséquences :
- matérielles,
- financières,
- voire humaines !
9
Introduction
Ratage (1) Ariane V - vol 501.
Le 4 juin 1996, 40 secondes après l’allumage, la fusée Ariane V s’est
auto -détruite. Les raisons :
1. Un bout de code d’Ariane IV (concernant le positionnement
et la vitesse de la fusée) repris dans Ariane V
2. il contenait une conversion d’un flottant sur 64 bits en un
entier signé sur 16 bits
3. pour Ariane V, la valeur du flottant dépassait la valeur
maximale pouvant être convertie
4. défaillance dans le système de positionnement
5. la fusée a “corrigé” sa trajectoire
6. une trop grande déviation l’a faite casser en deux.
10
Introduction
Ratage (2) Le Therac 25
Le Therac 25 était un accélérateur linéaire médical, destiné à
éliminer les tumeurs.
- toute la sécurité était logicielle
- plusieurs erreurs dans le programme
- certains patients ont reçu des doses jusqu’à 100 fois
supérieures à la normale !
Bilan :
- 6 accidents avérés,
- 4 morts,
- 2 ans pour mettre en cause le logiciel et retirer les machines.
11
Introduction
Il y a une différence entre la vérification et la validation formelle :
La vérification répond à la question : « est ce que le programme
ou le modèle se comporte correctement sans bug ? ».
La vérification utilise les prouvers de théorèmes . Exemple :
Système Coq.
La validation dit est ce que le programme ou le modèle répond
aux exigences , ou aux spécifications visées par les utilisateurs.
La validation utilise l’animation de modèle par le modèle
checking.
12
Introduction
Il y a une différence entre la vérification et la validation formelle :
La vérification répond à la question : « est ce que le programme
ou le modèle se comporte correctement sans bug ? ».
La vérification utilise les prouvers de théorèmes . Exemple :
Système Coq.
La validation dit est ce que le programme ou le modèle répond
aux exigences , ou aux spécifications visées par les utilisateurs.
La validation utilise l’animation de modèle par le modèle
checking.
13
Introduction
Vérification Formelle
Méthode basée sur les Méthode basé sur le
techniques de preuves modèle
Modèle checking
Le comportement du système est décrit dans un
formalisme ( automate, réseaux de pétri, algèbre
des processus ..) . Les propriétés à vérifier sont
décrites dans un autre formalisme, en général dans
une logique temporelle ( CTL, LTL ).
14
Introduction
Vérification Formelle
Méthode basée sur les Méthode basé sur le
techniques de preuves modèle
Modèle checking
Le comportement du système est décrit dans un
formalisme ( automate, réseaux de pétri, algèbre
des processus ..) . Les propriétés à vérifier sont
décrites dans un autre formalisme, en général dans
une logique temporelle ( CTL, LTL ).
15
Introduction
Pour ce qui est du Model-Cheking que nous aurons à développer
dans le cadre de ce cours, il s’agit de :
Construire un modèle M qui décrit le comportement du
système qu’on veut vérifier( par exemple les systèmes d’états
finis);
Exprimer les propriétés Φ , dans le formalisme de la logique
temporelle ;
La vérification à l’aide du Model-Cheking consiste à voir si :
M satisfait Φ ( M Φ)
16
Introduction
17
Introduction
Model Checking
18
Introduction
Etapes de vérification d’un système par modèle checking :
Etape 1:
Etablir les propriétés que l’on devra vérifier ;
Etape 2:
Construire un modèle formel du système;
Etape 3: Dérouler l’algorithme qui permet de vérifier que le modèle
satisfait les propriétés ,
Sinon, un compte exemple sera retourné.
19
Références
Support de cours « Vérification et validation formelle de
programmes », Khemliche Salem, Université Mouloud
Mammeri de Tizi-Ouzou, 2015/2016.
20
