Université Hassan 1er

Ecole Nationale des Sciences Appliquées - Berrechid

Contrôle et vérification des systèmes embarqués

Pr. Laila DAMRI

Année universitaire : 2024-2025

• 4
Introduction à la
vérification des
modèles – Model
Checking
Partie I
Introduction
Expression de besoin

Comment prouver que le contrôle du processus :

▪ est exempt de bugs ?
▪ est conforme aux attentes du cahier des charges ?

Scénario de test sur le réel ?

▪ très proche de l’utilisation nominale ;
▪ vue très limitée des possibilités du contrôle ;
▪ nécessite du matériel spécifique.

3
Introduction
Expression de besoin

Simulation par modèle ?

▪ long ;
▪ n’atteint pas tous les cas d’utilisations possibles.

Vérification formelle
▪ prouve que le programme de commande est conforme ;
▪ taux de couverture de 100% du comportement logiciel.
▪ MAIS vérification de modèles de programme et non de programmes.

4
Introduction
Vérification formelle du comportement d’un système

Comportement interdit
Comportement Désiré (CD)
▪ Ce que le système doit faire
Comportement Interdit (CI)
▪ Ce que le système ne doit pas faire Comportement du système
Comportement du système (CS)
▪ Ce que fait le système

Comportement désiré

5
Introduction
Vérification formelle du comportement d’un système
Comportement
interdit

Vérification formelle :
▪ Prouver que

Comportement désiré

Comportement du système

6
Introduction
Quelques bugs célèbres

➢ 1940 Mark-I : une erreur de calcul est détectée. Une inspection de la machine montre un
court-circuit d un insecte (bug).

➢ 1985 Appareil de radiothérapie Therac-25.

Erreur de dosage dans des traitements du cancer (morts).

➢ 1990 Processeur arithmétique de l’Intel Pentium II.

≈ 475M$ pour remplacer les processeurs.

7
û
à
Introduction
Quelques bugs célèbres

➢ 1995 Système de gestion des bagages l’aéroport de Denver.

Retard d’ouverture de 9 mois, ≈ 1M$/jour.

➢ 1996 Explosion d’Ariane 5 lors de son vol inaugural.

Utilisation d’un contrôleur d’Ariane 4 ne supportant pas les données d’accélérations
d’Ariane 5 (dépassement de capacité).

8
à
Introduction
Détection des bugs

La détection des bugs peut se faire via quelques approches complémentaires :

➢ Revue de code :
Parcourir manuellement le code et essayer de détecter l’anomalie.

􏰄
Introduction
Détection des bugs

La détection des bugs peut se faire via quelques approches complémentaires :

➢ Tests
▪ Simulation de scenarios et peut être réalisée :
- sur la spécification - sur la réalisation
- sur le tout
- sur une partie
- automatiques ou non

10

􏰄
Introduction
Détection des bugs

La détection des bugs peut se faire via quelques approches complémentaires :

➢ Tests
▪ Tests unitaires
- locaux
- peuvent être orthogonaux l’application
- automatiques ou non

11
à
􏰄
Introduction
Détection des bugs

La détection des bugs peut se faire via quelques approches complémentaires :

➢ Tests
▪ Tests généraux
- via des plates-formes d’exécution outillées (ex : valgrind)

12

􏰄
Introduction
Détection des bugs

La détection des bugs peut se faire via quelques approches complémentaires :

➢ Model-checking
▪ Méthode formelle de vérification

Les tests doivent être refaits après modifications pour détecter les régressions.

13

􏰄
Introduction
Test versus vérification

➢ Test : partir d’une donnée, un seul chemin est test .

➢ Vérification : tous les chemins sont testés.

Test Vérification 14
à
é
Introduction
Modélisation et vérification

➢ Abstraction du système concret et simulation de ce modèle

▪ Modélisation de systèmes : automates (systèmes de transitions)
▪ Simulation du modèle : langages des automates (traces d’exécutions)
▪ Modélisation des propriétés attendues des systèmes (Logiques)

➢ Vérification automatique par Model-checking

▪ Technique automatique
▪ Exploration complète des configurations des systèmes
▪ Retour de contre-exemple lorsqu’une propriété n’est pas vérifiée

15
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 1 : Montre à affichage numérique hh:mm

Avec 60 × 24 = 1440 états, nous pouvons représenter tous les états atteignables de notre
montre.

16
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 1 : Montre à affichage numérique hh:mm

Avec 60 × 24 = 1440 états, nous pouvons représenter tous les états atteignables de notre
montre.

17
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 2 : Digicode à trois touches A,B et C

La porte s’ouvre quand ABA est saisi. Le digicode est dans son état initial après saisie d’un
mauvais code.

18
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 2 : Digicode à trois touches A,B et C

La porte s’ouvre quand ABA est saisi. Le digicode est dans son état initial après saisie d’un
mauvais code.

19
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 3 : Compteur modulo 4

Il effectue les opérations suivantes :
✓ inc : incrémente de 1 le compteur
✓ dec : diminue de 1 le compteur
1 état par valeur du compteur : 4 états

20
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 3 : Compteur modulo 4

Il effectue les opérations suivantes :
✓ inc : incrémente de 1 le compteur
✓ dec : diminue de 1 le compteur
1 état par valeur du compteur : 4 états

21
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 4 : Canal FIFO de capacité 2 sur l’alphabet {a,b}

Il effectue les opérations suivantes :
▪ in(x) : enfiler la lettre x si le canal n’est pas plein
▪ out(x) : défiler la lettre x si le canal n’est pas vide
1 état par configuration possible du canal

22
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 4 : Canal FIFO de capacité 2 sur l’alphabet {a,b}

Il effectue les opérations suivantes :
▪ in(x) : enfiler la lettre x si le canal n’est pas plein
▪ out(x) : défiler la lettre x si le canal n’est pas vide
1 état par configuration possible du canal : 7 états

23
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 5 : Variable booléenne

On peut effectuer les opérations suivantes :
▪ b = vrai, b =faux: test de la valeur de la variable b
▪ b := vrai, b := faux : affectation de la variable b
1 état par valeur

24
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 5 : Variable booléenne

On peut effectuer les opérations suivantes :
▪ b = vrai, b =faux: test de la valeur de la variable b
▪ b := vrai, b := faux : affectation de la variable b
1 état par valeur

25
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 6 : Programme séquentiel

1: While true do
if not b then
begin
2: b:= true;
3: proc ;
4: b := false;
end
od

26
Introduction
Modélisation et vérification : exemples de modélisation

Exemple 6 : Programme séquentiel

1: While true do
if not b then
begin
2: b:= true;
3: proc ;
4: b := false;
end
od

27
Système de transition - automate
Présentation

➢ Pour appliquer des techniques de model-checking, il est souvent nécessaire de déplier les
comportements de l’automate.

➢ On obtient un système de transitions qui incorpore les valeurs des variables d’états dans
ses états.

C’est encore un automate

28
Système de transition - automate
Système de transitions
Noté aussi →

Un système de transitions est un triplet A = ⟨S , I, R ⟩ où :

▪ S est un ensemble d’états fini ou infini.

▪ I ⊆ S : ensemble des états initiaux.

▪ R ⊆ S × S est un ensemble de relations (transitions) entre paires d’états (s, s’).

(s,s′) ∈ R signifie qu’il existe une transition faisant passer le système de l’état s à l’état s′.

29
Système de transition - automate
Système de transitions

Prédécesseur et successeur

Soit T = (S, → , I) un système de transition.

On écrit s → t pour dénoter (s, t) ∈ →.
Si s → t, on dit que s est un prédécesseur immédiat de t, et que t est un successeur immédiat
de s.

L’ensemble des successeurs et prédécesseurs immédiats d’un état s ∈ S sont respectivement

dénotés :

Nous disons qu’un état s ∈ S est terminal si Post(s) = ∅.

30
Système de transition - automate
Système de transitions

Prédécesseur et successeur

L’ensemble des successeurs et prédécesseurs d’un état s ∈ S sont respectivement dénotés:

correspond l’état t est accessible à partir de l’état s en zéro, une ou plusieurs

transitions.

est la fermeture réflexive et transitive de →.

31
Système de transition - automate
Système de transitions

Prédécesseur et successeur
Exemple:
On considère le système de transition suivant :

Pre(s0) = Pre(s2) =
Post(s0) = Post(s2) =
Pre∗(s0) = Pre∗(s2) =
Post∗(s0) = Post∗(s2) =
Pre(s1) =
Post(s1) =
Pre∗(s1) =
Post∗(s1) =
32
Système de transition - automate
Système de transitions

Prédécesseur et successeur
Exemple:
On considère le système de transition suivant :

Pre(s0) = {s0} Pre(s2) = {s0, s1, s2}

Post(s0) = {s0, s1, s2} Post(s2) = {s2},
Pre∗(s0) = {s0} Pre∗(s2) = {s0, s1, s2}
Post∗(s0) = {s0, s1, s2} Post∗(s2) = {s2}
Pre(s1) = {s0}
Post(s1) = {s2}
Pre∗(s1) = {s0, s1}
Post∗(s1) = {s1, s2}
33
Système de transition - automate
Système de transitions

Explosion combinatoire
➢ La taille d’un système de transition fini croît rapidement en fonction du système concret
sous-jacent.

Exemple :
Un système de transition modélisant un programme avec n variables booléennes peut
posséder jusqu’à 2n états.

➢ Ce phénomène est connu sous le nom d’explosion combinatoire.

34
Système de transition - automate
Système de transitions

Explosion combinatoire
➢ Il existe plusieurs mesures pour contrer cette explosion :
▪ Les outils de vérification génèrent normalement les systèmes de transitions à la volée
plutôt qu’exhaustivement.
▪ D’autres techniques peuvent être utilisées lors de la modélisation ou de la
vérification :
o Abstraction: ignorer les données jugées non importantes pour réduire la taille du
système de transition (de façon manuelle ou automatique).
o Vérification symbolique: utiliser des structures de données pouvant représenter
plusieurs états symboliquement et manipuler directement ces structures.
o Approximations: calculer un sous-ensemble ou sur-ensemble des états
accessibles de façon symbolique afin de prouver la présence ou l’absence
d’erreurs. 35
Système de transition - automate
Système de transitions

Exemple:

S = {s0, s1, s2, s3, s4}

I = {s0}
R = {(s0, s0), (s0, s1), (s0, s2), (s2, s3), (s3, s4), (s4, s3)}

36
Système de transition - automate
Système de transitions

Chemin ou séquence
➢ Un chemin c de longueur n (noté ∣c∣ = n) est une suite de transitions :
s1→ s2 → s3 → ..→ sn

➢ Un chemin infini est une suite infinie de transitions

37
Système de transition - automate
Système de transitions

Chemin ou séquence
Vocabulaire

Soit S un ensemble

▪ S* est l’ensemble des séquences finies sur S.

▪ Sw est l’ensemble des séquences infinies sur S.

▪ Σi est le ième (à partir de 0) élément d’une séquence σ.

38
Système de transition - automate
Système de transitions

Chemin ou séquence
Conventions de représentation

▪ Une séquence s est notée sous la forme : ⟨s1 → s2 → …⟩.

▪ ⟨⟩ : la séquence vide.

39
Système de transition - automate
Système de transitions

Chemin ou séquence
Pour une séquence finie σ

▪ σ* est l’ensemble des séquences finies produites par la répétition arbitraire de σ.

▪ σ+ = σ∗\{⟨⟩}.

▪ σω est la séquence infinie produite par la répétition infinie de σ.

40
Système de transition - automate
Système de transitions

Trace
Traces finies

Soit ⟨S, I, R⟩ un système de transitions.

On appelle trace finie une séquence finie σ ∈ S* telle que :

▪ σ = ⟨s0 →s1 →...→sn−1 →sn⟩

▪ ∀i ∈ [0..n[: (si,si+1) ∈ R

41
Système de transition - automate
Système de transitions

Trace
Traces finies maximales

Soit ⟨S, I, R⟩ un système de transitions.

Une trace finie ⟨s0 →s1 →...→sn−1 →sn⟩∈S* est maximale ssi il n’existe pas d’état
successeur à sn, i.e. ∀s ∈ S : (sn, s) ∈/ R.

Une trace maximale va le plus loin possible.

42
Système de transition - automate
Système de transitions

Trace
Traces infinies

Soit ⟨S, I, R⟩ un système de transitions, et s0 ∈ S.

On appelle trace infinie à partir de s0 un élément tr ∈ Sω tel que :

tr = ⟨s0 →s1 →s2...⟩ ∀i ∈ N : (si,si+1) ∈ R

43
Système de transition - automate
Système de transitions

Exécutions

Soit S = ⟨S , I , R ⟩ un système de transitions.

Une exécution σ = ⟨s0 → . . .⟩ est une trace infinie ou finie maximale telle que s0 ∈ I.

Exec(S) est l’ensemble des exécutions de S.

On a une (seule et unique) exécution vide ⟨⟩ ssi I = ∅.

44
Système de transition - automate
Système de transitions

Exemple

Traces (s1) = ⟨s1⟩

Traces (s3) = ⟨(s3 → s4)ω⟩
Traces (s2) = ⟨s2 → (s3 → s4)ω⟩
Traces (s0) = ⟨s0ω⟩, ⟨s0+ → s1⟩, ⟨s0+ → s2 → (s3 → s4)ω⟩

s0 → s0 → s2 → s3 est une trace finie non maximale

Exec (S) = Traces (s0)

45
Système de transition - automate
Exercice d’application 1

Donner les traces suivantes :

Traces (s2) =

Traces (s0) =

Exec (S) =

46
Système de transition - automate
Exercice d’application 2

Donner les traces suivantes :

Traces (s2) =

Traces (s0) =

Traces (s1) =

Exec (S) =

47
Système de transition - automate
Système de transitions étiqueté

Un système de transitions étiqueté est un couple A = ⟨S , T , Σ⟩ où :

▪ S est un ensemble d’états fini ou infini

▪ T⊆S×Σ×S est un ensemble de transitions fini ou infini

▪ Σ est un ensemble d’actions

Trace

Si c est un chemins alors la suite une trace

48
Système de transition - automate
Système de transitions étiqueté

Structures de Kripke

49
Système de transition - automate
Structures de Kripke

Un système de transitions où : K = (S, I, T, P, L)

• S : ensemble d’états (states)

• I ⊂ S : ensemble d’états initiaux
• T ⊂ S×S : relation de transition totale gauche
∀s∈S. ∃s’∈E. sTs’ → chemins infinis pour T
• P = {p, q, ...} : ensemble de prédicats atomiques
• L : S→2P : fonction d’étiquetage
L(s) = {p, r,...} ensembles des prédicats vrais en s

Rappel
• Chemin : π = s0 →s1 →s2→...
50
• Suffixe : π[n] = sn →sn+1 →sn+2→...
à
Système de transition - automate
Structures de Kripke

Exemple de structure de Kripke

Propriétés :
P1 : p et q ne sont jamais vraies en même temps
P2 : tout q est immédiatement suivi d’un r
P3 : tout p est immédiatement suivi d’un q
P4 : tout chemin infini depuis un état initial atteint r
P5 : tout chemin infini depuis un état initial atteint p 51
Système de transition - automate
Structures de Kripke

Exemple de structure de Kripke

Propriétés :
P1 : p et q ne sont jamais vraies en même temps satisfaite
P2 : tout q est immédiatement suivi d’un r
P3 : tout p est immédiatement suivi d’un q
P4 : tout chemin infini depuis un état initial atteint r
P5 : tout chemin infini depuis un état initial atteint p 52
Système de transition - automate
Structures de Kripke

Exemple de structure de Kripke

Propriétés :
P1 : p et q ne sont jamais vraies en même temps satisfaite
P2 : tout q est immédiatement suivi d’un r satisfaite
P3 : tout p est immédiatement suivi d’un q
P4 : tout chemin infini depuis un état initial atteint r
P5 : tout chemin infini depuis un état initial atteint p 53
Système de transition - automate
Structures de Kripke

Exemple de structure de Kripke

Propriétés :
P1 : p et q ne sont jamais vraies en même temps satisfaite
P2 : tout q est immédiatement suivi d’un r satisfaite
P3 : tout p est immédiatement suivi d’un q non satisfaite
P4 : tout chemin infini depuis un état initial atteint r
P5 : tout chemin infini depuis un état initial atteint p 54
Système de transition - automate
Structures de Kripke

Exemple de structure de Kripke

Propriétés :
P1 : p et q ne sont jamais vraies en même temps satisfaite
P2 : tout q est immédiatement suivi d’un r satisfaite
P3 : tout p est immédiatement suivi d’un q non satisfaite
P4 : tout chemin infini depuis un état initial atteint r satisfaite
P5 : tout chemin infini depuis un état initial atteint p 55
Système de transition - automate
Structures de Kripke

Exemple de structure de Kripke

Propriétés :
P1 : p et q ne sont jamais vraies en même temps satisfaite
P2 : tout q est immédiatement suivi d’un r satisfaite
P3 : tout p est immédiatement suivi d’un q non satisfaite
P4 : tout chemin infini depuis un état initial atteint r satisfaite
P5 : tout chemin infini depuis un état initial atteint p non satisfaite 56