Technique de Test Logiciel ( TTL )

Université de Biskra
Département d’informatique

1er année Master

Option : GLSD

Module: TTL

Présenté par
Dr. Ouaar Hanane

1
Année universitaire 2016/2017
 Chapitre 4:

Techniques de
vérification formelle

2
Chapitre 4 : Technique de vérification formelle
Introduction
la spécification de certain système se ramène à l'étude des relations
qui existent entre plusieurs composants caractérisant le système
étudié.

La modélisation est une activité technique qui s’inscrit dans de

nombreux processus d’ingénierie, son but est de fournir une
représentation approchée du système ou du produit que l’on veut
analyser, concevoir ou fabriquer.

De cet effet, il existe dans la littérature des catégories des

spécification nous allons étudier : la spécification semi formelle tel
que UML, la spécification formel tel que les RDP, les automates
d’états finis et des langages formel tel que la logique temporel.

3
Chapitre 4 : Technique de vérification formelle
Types des approches de vérification formelle

Langages de
Spécification

Semi-formels Formels Informels

Modèle à
Algebrique La logique
états

Model-Checking
4
Chapitre 4 : Technique de vérification formelle
Les approches semi-formelles (UML)

Les points forts :

- Sa notation graphique permet d'exprimer visuellement une solution
objet, ce qui facilite la comparaison et l'évaluation de solutions.
- Limite les ambiguïtés et les incompréhensions.
- Permet le gain de précision, encourage l'utilisation d'outils.
- Cadre l'analyse et facilite la compréhension de représentations
abstraites complexes.
-Son caractère polyvalent et sa souplesse en font un langage universel.

Les points faibles :

- La mise en pratique d'UML nécessite un apprentissage et passe par une
période d'adaptation.
- La lourdeur (relative) de sa mise en place au sein de n'importe quel
processus. 5
Chapitre 4 : Technique de vérification formelle
Principes des approches de vérification formelle

:
Les méthodes formelles sont des techniques
alternatives, fondées sur des base mathématiques,
permettant la spécification et le développement de
systèmes, ainsi que la vérification automatique de
propriétés.

6
Chapitre 4 : Technique de vérification formelle

logique de Hoare

7
Chapitre 4 : Technique de vérification formelle
Spécification logique: logique de Hoare
•Une méthode formelle définie par le chercheur en
informatique britannique Tony Hoare en 1969 .

•La méthode met en place un formalisme logique permettant

de raisonner sur la correction des programmes
informatiques.

•La logique Hoare a des axiomes pour toutes les instructions

( si , sinon ,boucle .. Etc )

* Même des règles pour les procédures, les sauts, les

pointeurs 8
Chapitre 4 : Technique de vérification formelle

Le triplet Hoare :

{P} i {Q}

P : pré-condition i: exécution Q:post-condition

Example :
Un exemple valide :{x>0} x :=x+1 {x>0} // car (x>0)+1 est tjrs >0
›Un exemple non-valide :{x>0} x :=x-1 {x<2} //car (x>0)-1
n’est pas tjrs <2

9
Chapitre 4 : Technique de vérification formelle

Critique :

1-Le système de Hoare est complexe à utiliser car:

-Règles lourdes à appliquer.
-Taille des arbres de preuve.

2-La logique de Hoare permet de démontrer qu’un

programme vérifie une spécification .

10
Chapitre 4 : Technique de vérification formelle
Les approches de vérification formelle

Model checking

11
Chapitre 4 : Technique de vérification formelle
Spécification par model : Model checking
Principe: Un vérificateur de modèle prend le modèle extraites du
système et les propriétés en entrée et recherche de manière
exhaustive les erreurs éventuelles.
vérifier si un système S satisfait une propriété P.

Domaines:
– protocoles de communication (les précurseurs)
– circuits électroniques
– algorithmes distribués
– programmes réactifs et temps-réel

Il s'agit d'un graphe : un sommet représente un état du système

et chaque arc représente une transition
12
Chapitre 4 : Technique de vérification formelle
Spécification par model : Model checking
Les logiques temporelles les plus utilisée dans
model cheking :

Il existe plusieurs logiques temporelles :

* LTL (linear tomporal logic)
* CTL* (computational tree logic) .. Etc..

La propriété à vérifier est écrite par une formule

de logique temporelle.

13
Chapitre 4 : Technique de vérification formelle
Spécification par model : Model checking
Etapes :
Phase de modélisation :
Modéliser le système à l'étude
Formaliser la propriété à vérifier
Phase d'exécution :
Exécuter le model checker pour vérifier la validité de la propriété dans
le modèle
Phase d'analyse :
Propriété satisfaite ? vérifier la propriété suivante .
Propriété violée ?
1. analyser le contrexemple généré par simulation.
2. affiner le modèle, le design du modèle ou la propriété . . . et
répéter
la procédure pas assez de mémoire ?
14
 essayer de réduire le modèle et tester à nouveau
Chapitre 4 : Technique de vérification formelle
Spécification par model : Model checking
Exemples :distributeur de café

15
Chapitre 4 : Technique de vérification formelle
Spécification par model : Model checking

Qualités:

Fiabilité: Assure la propriété de sureté qui assure la fiabilité

Exhaustivité: Vérification exhaustive
Déploiement: Durant le développement
Coût: Moins cher

16
Chapitre 4 : Technique de vérification formelle
Techniques
Critère
Hoare logic Model-cheking
+
-
Automatisation Basé sur l’
Non-automatisable
automastisation
Preuves conception conception
+++ +
Applications
illlimité limités
- +
comprehension
Difficiles moyen
+
+++
Prend du temps car c’est
rapidité plus rapide par rapport à
des preuves ecrites a la
d’autres techniques
main
validation ++ +
Assisté par ordinateur - + 17
Chapitre 4 : Technique de vérification formelle

Spécification algébrique

18
Chapitre 4 : Technique de vérification formelle
Spécification algébrique:
Les spécifications algébriques sont une technique permettant de définir
le comportement (c’est-à-dire spécifier) des logiciels au travers des
structures de données qu’ils manipulent (les listes, les files, les piles,
les arbres, etc.).
La manière la plus commune de caractériser une spécification SP est de
donner un ensemble d’axiomes Ax composé de formules de la logique
des prédicats du premier ordre.
On note alors SP = (Σ, Ax) et on dit que SP est une spécification
axiomatique.
19
Chapitre 4 : Technique de vérification formelle
Spécification algébrique:
exemple : les piles
Soit une pile :
Les opérations vide et empiler sont les constructeurs de pile.

L’opération dépiler permet d’enlever le dernier élément empilé dans

une pile. L’opération haut renvoie ce dernier élément sans le supprimer.

L’opération hauteur renvoie la hauteur de la pile (le nombre

d’éléments).
20
Chapitre 4 : Technique de vérification formelle
Spécification algébrique:
exemple : les piles
Soit ΣPiles = (SPiles, FPiles, VPiles) une signature équationnelle telle
que :

SPiles = {entier, pile}

FPiles = {0 : entier, succ : entier → entier,
vide :→ pile,
empiler : entier × pile → pile,
depiler : pile → pile,
haut : pile → entier,
hauteur : pile → entier}
21
Chapitre 4 : Technique de vérification formelle
Spécification algébrique:
exemple : les piles
La spécifications des piles Piles est composé de la signature ΣPiles et de
l’ensemble AxPiles d’axiomes suivant :

depiler(vide) = vide
depiler(empiler(x, p)) = p
haut(vide) = 0
haut(empiler(x, p)) = x
hauteur(vide) = 0
22
hauteur(empiler(x, p)) = succ(hauteur(p))
Chapitre 4 : Technique de vérification formelle
Limitations de la vérification formelle :

Pas de notion absolue de correction.

La correction est toujours relative à une spécification donnée.

Difficile et coûteux d’écrire des spécifications formelles.

En pratique, on ne spécifie pas formellement toutes les
fonctionnalités mais les propriétés de sûreté comme la bonne
formation des données (accès hors des bornes, déréférencement
du pointeur null, etc.), absence d’exceptions non détectées, les
parties critiques du logiciel etc.

Coûteux également de faire des preuves (mais on gagne sur le

temps de test).
23
Chapitre 4 : Technique de vérification formelle

Les Machines à Etats Finis

24
Chapitre 4 : Technique de vérification formelle
Les Machines à Etats Finis (FSMs)

Une machine à états finis est un modèle dynamique, c'est à dire qui
évolue dans le temps.
Cette évolution se traduit par des changements d’états en fonction des
entrées permettant d’activer les transitions. Ceci étant, l’exécution
commence toujours par un état initial, puis, en fonction de l’activation
des transitions, la machine change d’état.
A noter qu’à tout instant le système doit se trouver dans un état unique.

25
Chapitre 4 : Technique de vérification formelle

Les FSMs sont utilisés pour décrire le comportement du système

sous test.

Les différents chemins (séquences de transitions) dans les FSMs

s’apparentent à des scenarios de test.

Ainsi, les FSMs ont largement été utilisés comme modèles d’entrée

pour la génération automatique de cas de test

26
Chapitre 4 : Technique de vérification formelle
Les Machines à Etats Finis (FSMs)
Présentation un FSM est généralement représenté sous forme graphique avec des
états (nœuds) et des transitions (arcs). Typiquement un FSM est un 4-uplet (E, T, In,
Out) où

E est un ensemble fini d’états

T est un ensemble fini de transitions.
In est un ensemble d’entrées provoquant les transitions.
Une entrée peut par exemple représenter une expression booléenne définie sur une
transition pour spécifier les conditions de passage d’un état vers un autre.
Out est un ensemble de sorties qui peuvent se produire lors des transitions.
Par exemple, une sortie peut représenter une action provoquée par le passage d’un état
vers un autre. 27
Chapitre 4 : Technique de vérification formelle
Les Machines à Etats Finis (FSMs)

28
Chapitre 4 : Technique de vérification formelle
Avantages et Limitations
L’un des avantages des FSMs est sans doute sa notation qui est
intuitive et graphique. Les différents chemins, qui peuvent être vus
comme des scenarios de test, sont facilement repérables sur le modèle.
Aussi, les FSMs sont très connus et utilisés aussi bien par les
développeurs et les testeurs que par les clients.

Cependant, les FSMs souffrent en particulier de l’explosion

combinatoire (du nombre d’états et de transitions). En effet, pour
modéliser certains systèmes, le nombre d’états et de transitions requis
peut être très important. Ce qui rend le modèle complexe et difficile à
29
exploiter.
Chapitre 4 : Technique de vérification formelle
Les approches de vérification formelle

Réseaux de Pétri

30
Chapitre 4 : Technique de vérification formelle
Les Réseaux de Pétri
Présentation
Les réseaux de Pétri (Petri nets) [73],[74] inventés par Carl Adam Petri
en 1962, sont une forme spéciale de graphe orienté possédant deux types
de nœuds (repartis en deux groupes distincts) et des arcs reliant un type
de nœud à l’autre. Typiquement, un réseau de Pétri est composé de
trois groupes d’éléments :
Des nœuds de type P appelés places qui représentent souvent les
possibles états ou conditions nécessaires à l’accomplissement d’une
action.
Des nœuds de type T appelés transitions qui représentent souvent
des événements ou des actions causant les changements d’états du
système.
Des arcs orientés avec chacun connectant une place à une transition,
ou une transition à une place.
31
Chapitre 4 : Technique de vérification formelle
On appellera entrées d’une transition tous les prédécesseurs de cette
transition dans le graphe. De même tous les successeurs de cette
transition dans le graphe seront appelés sorties.

Par exemple, le réseau de Pétri de la Figure (a) comporte trois

places p1, p2 et p3, une transition t1 et trois arcs (p1, t1), (p2, t1) et
(t1, p3). Ainsi p1 et p2 représentent les entrées de t1, et p3 sa sortie.

32
Chapitre 4 : Technique de vérification formelle
L’exécution d’un réseau de Pétri se traduit par des changements
d’états.

Un changement d’état est caractérisé par un mouvement d’un ou de

plusieurs jetons, de places en places, en considérant le
déclenchement d’une ou des transitions.

Le déclenchement d’une transition peut représenter une

occurrence d’un événement ou d’une action. Par ailleurs le
déclenchement d’une transition ne peut se produire que si elle est
au préalable active, c'est-à-dire que chacune de ses entrées contient
au moins un jeton.

Ainsi le déclenchement se traduit par le déplacement des jetons des

entrées de la transition vers ses sorties.
33
Chapitre 4 : Technique de vérification formelle

Considérons maintenant le réseau de Pétri de la Figure (b), la

présence d’un jeton dans chacune des entrées de t1 rend cette
transition active. Ça n’aurait pas été le cas si p1 et/ou p2
n’avait pas de jeton. Le déclenchement de t1 produit le déplacement
des jetons de p1 et p2 vers p3 (Figure 2.5 (c)).

Il existe plusieurs variantes de réseaux de Pétri, on distingue entre

autres :

les réseaux de Pétri colorés (coloured Petri nets)

les réseaux de Pétri temporels (timed Petri nets) .

34
Chapitre 4 : Technique de vérification formelle

Les réseaux de Pétri sont souvent utilisés pour décrire le comportement

de systèmes complexes, en particulier les systèmes distribués. Ainsi, ils
ont été utilisés comme modèles d’entrée pour la génération automatique
de cas de test.
Dans [77] les réseaux de Pétri sont d’abord utilisés pour décrire le
comportement des éléments du système sous test. Ensuite, l’approche
propose des critères de couverture (par exemple, couverture des
transitions du modèle). Ainsi, en fonction du critère choisi, un arbre de
test est généré à partir du réseau de Pétri et les tests sont générés en
parcourant l’arbre de la racine aux feuilles.
Dans [78] les réseaux de Pétri colorés (coloured Petri nets) ont été
utilisés pour spécifier un système de contrôle de train. Ensuite à partir du
réseau de Pétri une approche permettant de générer des tests à partir de
ce formalisme est présentée.
35
Chapitre 4 : Technique de vérification formelle

Avantages et Limitations
Les réseaux de Pétri offrent une notation puissante permettant de
modéliser et/ou de simuler des systèmes complexes, par exemple,
des systèmes distribués. Cependant, ils sont peu utilisés et peu
connus dans le domaine de la génération de cas de test.
La raison est que la notation est très complexe, peu intuitive et
difficile à maintenir (par exemple s’il y a des modifications à
apporter au modèle suite à une modification des spécifications).

36
Chapitre 4 : Technique de vérification formelle
Les approches de vérification formelle

Modèles Stochastiques
(chaines de Markov)

37
Chapitre 4 : Technique de vérification formelle
Modèles Stochastiques (chaines de Markov)
Présentation

Les modèles stochastiques permettent de représenter un système en

se basant sur des notions probabilistes. Les chaines de Markov
[79],[80] sont un exemple typique des modèles stochastiques. Ils
permettent globalement de représenter l’évolution d’un système dans
le temps en utilisant des modèles de transitions associés à des
probabilités (sur les transitions).

L’une des propriétés importantes des chaines de Markov est

l’absence de mémoire, c'est-à-dire que le prochain état du système
ne dépend que de l’état courant de celui-ci et non des états passés.

38
Chapitre 4 : Technique de vérification formelle
L’exemple de la Figure présente une chaine de Markov (discrète) à
deux états (A et B) et quatre transitions, chacune associée à une
probabilité. Ainsi, à partir de l’état A, le système passe dans l’état B
avec une probabilité de 2/3 ou reste dans l’état A avec une probabilité
de 1/3. Dans l’état B le système passe dans l’état A avec une probabilité
de 1/2 ou reste dans l’état B avec également une probabilité de 1/2.
On remarquera que la somme des probabilités associées aux transitions
sortantes d’un état quelconque vaut 1.

39
 Application :

Modélisation formelle d’un

bruleur à gaz par les AEF
temporisés en utilisant
UPPAAL

40
Modélisation formelle d’un bruleur à gaz par les AEF temporisés en utilisant UPPAAL

Exemple de bruleur de gaz

41
Modélisation formelle d’un bruleur à gaz par les AEF temporisés en utilisant UPPAAL

Modèles de processus contrôleur

42
Modèle de processus allumeur
Modélisation formelle d’un bruleur à gaz par les AEF temporisés en utilisant UPPAAL

Résultat de vérification formelle par l’UPPAAL 43

Modélisation formelle d’un bruleur à gaz par les AEF temporisés en utilisant UPPAAL

Simulation de comportement synchronisé

44
Modélisation formelle d’un bruleur à gaz par les AEF temporisés en utilisant UPPAAL

Résultat de la simulation synchronisée

45
 Conclusion
Les applications sont de plus en plus complexes, les
volumes de données sont de plus en plus grands...
Les tests sont aujourd’hui au centre de tous les intérêts :
de nombreux progiciels ont vu le jour pour tester,
gérer les versions…
Des sociétés ont investi dans la création d’un service
interne, véritable structure de tests. Rien ne peut être
mis en production sans être validé par ce service.
L’Internet mobile, nouveau mode d’information et
nouveau challenge pour les entreprises, est un support
graphique différent nécessitant une programmation
adaptée et donc des tests complémentaires. 46
 Bibliographie
• Cours 1: Prof. Youness Boukouchi, les fondamentaux
du test logiciel, ENSA d'Agadir, 2017.
• Cours 2: Stefano Zacchiroli, Génie Logiciel Avancé –
Introduction, Paris7, 2011.
• Cours 3: Vérification & Validation, Philippe Collet,
université de Nice, 2008.
• Thèse : SekouKangoye, Elaboration d’une approche
de vérification et de validation de logiciel
embarqué automobile, basée sur la génération
automatique de cas de test. Université d’Angers,
2017.

47