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 II
Model checking
Introduction

➢ Dans la conception logicielle et matérielle de systèmes complexes, plus de temps et

d'efforts sont consacrés à la vérification qu'à la construction.

➢ Des techniques sont recherchées pour réduire et faciliter les efforts de vérification tout en
augmentant leur couverture.

➢ Les méthodes formelles offrent un grand potentiel pour obtenir une intégration précoce
de la vérification dans le processus de conception, pour fournir des techniques de
vérification plus efficaces et pour réduire le temps de vérification.

3
Model checking
Introduction

➢ Les méthodes formelles peuvent être considérées comme «les mathématiques appliquées
pour la modélisation et l'analyse des systèmes ».

➢ Objectif : établir l'exactitude du système avec une rigueur mathématique.

➢ Les méthodes formelles sont l'une des techniques de vérification «hautement

recommandées» pour le développement logiciel de systèmes critiques pour la sécurité
conformément, par exemple, à la norme de bonnes pratiques de la CEI (Commission
électrotechnique internationale) et aux normes de l'ESA (Agence spatiale européenne).

4
Model checking
Introduction

➢ Les techniques de vérification basées sur des modèles sont basées sur des modèles
décrivant le comportement possible du système d'une manière mathématiquement précise
et sans ambiguïté.

➢ Il s'avère que - avant toute forme de vérification - la modélisation précise des systèmes
conduit souvent à la découverte des ambiguïtés et des incohérences dans les
spécifications informelles des systèmes. De tels problèmes ne sont généralement
découverts qu'à un stade beaucoup plus tardif de la conception.

5
Model checking
Introduction

➢ Les modèles système sont accompagnés d'algorithmes qui explorent systématiquement

tous les états de ces modèles.

Cela fournit la base de toute une gamme de techniques de vérification allant d'une
exploration exhaustive (vérification du modèle) à des expériences avec un ensemble
restrictif de scénarios dans le modèle (simulation), ou en réalité (test).

6
Model checking
Introduction

7
Model checking
Introduction

➢ Le model checking est une technique de vérification qui explore tous les états possibles
du système de manière brutale.

➢ Semblable à un programme d'échecs informatique qui vérifie les mouvements possibles,

un model checker, l'outil logiciel qui effectue la vérification du modèle, examine tous les
scénarios système possibles de manière systématique.

➢ De cette manière, on peut montrer qu'un modèle de système donné satisfait vraiment une
certaine propriété.

8
Model checking
Définitions

➢ « Model …
▪ connaître ou caractériser tous les états d’évolution du programme de contrôle
nécessaire la vérification.
▪ Exemple : le graphe des situations accessibles d’un GRAFCET ou d’un réseau de
Pétri.

➢ ... - Checking »
▪ vérifier des propriétés sur ces états ou la relation entre ces états.

➢ État
▪ Valeur des variables un instant donn .

9
à
à
é
Model checking
Vie du système et model checking

10
Model checking
Principe de model checking

11
Model checking
Principe de model checking

12
Model checking
Approches du model checking

➢ Le model checking utilise le même principe des approches reconnues dans la conception
d’un système. À voir :

▪ L’approche Top-down (ou Top-bottom).

▪ L’approche Bottom-up (ou Bottom-top).

13
Model checking
Approches du model checking

14
Model checking
Les systèmes réactifs

Programme classique

Caractéristiques :

▪ Termine.
▪ Retourne un résultat.
▪ Données complexes, contrôle séquentiel (≈ simple).

Exemple : compilateur, algo de tri

15
Model checking
Les systèmes réactifs

Programme classique

Vérifier un programme classique :

▪ Aspect temporel toujours identique, mais les prédicats sur les données peuvent être
complexes.

“Le programme termine et le tableau est trié”

16
Model checking
Les systèmes réactifs

Système réactif

➢ Les systèmes informatiques modernes se caractérisent par le fait qu’ils sont le résultat
d’un processus d’intégration complexe.

➢ Les systèmes informatiques modernes sont décrits en interconnectant des sous-systèmes

au travers de connecteurs architecturaux définissant des politiques de communications.
On parle alors de systèmes réactifs.

➢ C’est des systèmes qui interagissent avec un environnement par le bais de capteurs (prise
d’information) et d’actionneurs (action).

17
Model checking
Les systèmes réactifs

Système réactif

Caractéristiques :

▪ Ne doit pas terminer.

▪ Ne retourne pas de résultat.

▪ Données simples, contrôle distribué (≈ complexe).

Exemple : protocole, OS

18
Model checking
Les systèmes réactifs

Système réactif

Vérifier un système réactif :

▪ Aspect temporel très varié mais les prédicats sur les données sont souvent simples.

▪ “Si un processus demande infiniment souvent à être exécuté, alors l’OS finira par l’exécuter”.

▪ “Il est toujours possible de revenir à l’état initial”.

▪ “Chaque fois qu’une panne est détectée, une alarme est émise”.

▪ “Chaque fois qu’une alarme est émise, une panne a été détectée”. 19
Model checking
Les systèmes réactifs

Système de transition = systèmes réactifs

Exemple :

20
Model checking
Les systèmes réactifs

Propriétés sur systèmes réactifs

▪ Accessibilité. Une certaine situation peut être atteinte

✓ x peut valoir 0, toute instruction peut être exécutée.

▪ Invariance. Chaque état local respecte une bonne propriété

✓ x ne vaut jamais 0, le tableau ne déborde jamais.

▪ Sûreté. Quelque chose de mauvais n’arrive jamais

✓ J’accède au fichier uniquement si j’ai entré le bon PIN.

21
Model checking
Les systèmes réactifs

Propriétés sur systèmes réactifs

▪ Vivacité. Quelque chose de bon finit par arriver

✓ Le programme termine, le message finit toujours par être transmis.
✓ Le programme revient toujours à l’état initial.

▪ Équité. Quelque chose de bon se répète infiniment souvent

✓ Si un processus demande toujours la main, il l’aura infiniment.

▪ Équivalence. comportementale Est-ce que 2 systèmes sont équivalents ?

✓ Système simple de référence VS système optimisé

22
Model checking
Les systèmes réactifs

Propri t s de s curit (safety)

Exemple : L’ascenseur ne peut pas voyager la porte ouverte

A vérifier
1. Au départ, l’ascenseur ferme sa porte avant de démarrer
2. Après un start, open ne doit jamais arriver jusqu’ stopped
3. Après un open, start ne doit jamais arriver jusqu’ closed

Condition d’environnement
L’ascenseur est initialement arrêté, porte ouverte

23
é
é
é
é
à
à
Model checking
Les systèmes réactifs

Propri t s de vivacité (liveness)

Exemple : L’ascenseur ramasse les passagers qui l’appellent

A vérifier
Après call[i], l’ascenseur finit par s’arrêter l’étage i et y ouvre sa porte avant de redémarrer.

Condition d’environnement
Quand il monte (rep. descend), l’ascenseur parcourt tous les étages dans l’ordre de la direction
donnée, jusqu’ l’ordre d’arrêt (qui doit nécessairement arriver).

24
é
é
à
à
Model checking
Les systèmes réactifs : récapitulatif

➢ Système réactif = système de départ, monde réel.

➢ Machine à état P = syntaxe du modèle.

➢ Système de transition S = sémantique de P.

➢ Structure de Kripke M = adaptation de S pour MC.

25
Logique temporelle
Mots infinis

Présentation
Soit Σ un alphabet fini. Un mot infini sur Σ est une suite infinie d’éléments de Σ. In note Σω
l’ensemble des mots infinis sur Σ.

Exemple :
u = ababbbbbbb …
• u(1) = a
• u(2) = b
• u(3) = a
• u(4) = b
• u(5) = b
• u(4) = b 26
Logique temporelle
Mots infinis

Produit
Impossible  produit de concaténation de deux mots infinis.

Possible  concaténer un mot fini v avec un mot infini u.

Exemple :
v = babba
u = ababbbb …
vu = babbaababbbb …

Ce produit s’étend aux langages.

{ab, ba, aa, bb}* {bbbb …}
27
Logique temporelle
Mots infinis

Notation ω
Soit L un langage de mots finis. On note Lω l’ensemble des mots infinis obtenus par concatenation
(infinie) de mot L.

Exemples :
• {ab}ω : ne contient que le mot abababababab…
• {ab, b, c}ω : tous les mots sur {a, b, c} où tout a est suivi d’un b.
• {aa, b, c}ω : tous les mots sur {a, b, c} où les blocs de a sont de longueurs paire.
• {b*a}ω : tous les mots sur {a, b}, contenant un nombre infini de a.

Si u est un mot infini non vide, alors uω désigne l’unique mot de {u}ω.

28
Logique temporelle
Présentation de la logique temporelle

➢ Permettent d’exprimer les propriétés sur séquences d’observations.

➢ Utilisation de connecteurs temporels et de quantificateurs sur les chemins.

➢ Deux approches :

o Temps linéaire : propriétés des séquences d’exécutions (futur déterminé).

o Temps arborescent : propriétés de l’ arbre d’exécutions (tous les futurs possibles).

29
Logique temporelle

Logique Temporelle Linéaire

LTL

30
Logique temporelle
Logique Temporelle Linéaire (LTL)

La logique du temps linéaire (Linear temporal logic) sert à la modélisation d’événements pour un
temps discret (non quantifié) et linéaire.

➢ Syntaxe.
➢ Sémantique (mots infinis).
➢ Autres opérateurs et exemples.

31
Logique temporelle
Logique Temporelle Linéaire (LTL)

Syntaxe
On considère un alphabet fini Σ. Une formule LTL est construite en utilisant :

1. Les lettres de Σ (comme formules atomiques).

Exemple :
a est une formule LTL.

32
Logique temporelle
Logique Temporelle Linéaire (LTL)

Syntaxe
On considère un alphabet fini Σ. Une formule LTL est construite en utilisant :

2. Les opérateurs booléens classiques :

Exemple :

est une formule LTL.

33
Logique temporelle
Logique Temporelle Linéaire (LTL)

Syntaxe
On considère un alphabet fini Σ. Une formule LTL est construite en utilisant :

3. L’opérateur temporel unaire ο (next).

Exemple :

est une formule LTL.

34
Logique temporelle
Logique Temporelle Linéaire (LTL)

Syntaxe
On considère un alphabet fini Σ. Une formule LTL est construite en utilisant :

4. L’opérateur temporel binaire U (until).

Exemple :

est une formule LTL.

35
Logique temporelle
Logique Temporelle Linéaire (LTL)

Sémantique (1/ 4)
On considère une formule LTL φ sur Σ. On dit qu’un mot infini u ∈ ∑ω satisfait φ à la position i
,noté
(i ∈ N * ) quand :

• ,

Exemple :

36
Logique temporelle
Logique Temporelle Linéaire (LTL)

Sémantique (2/ 4)
On considère une formule LTL φ sur Σ. On dit qu’un mot infini u ∈ ∑ω satisfait φ à la position i
,noté
(i ∈ N * ) quand :

• (idem pour les autres opérateurs booléens).

37
Logique temporelle
Logique Temporelle Linéaire (LTL)

Sémantique (3/ 4)
On considère une formule LTL φ sur Σ. On dit qu’un mot infini u ∈ ∑ω satisfait φ à la position i
,noté
(i ∈ N * ) quand :

• ,

Exemple :

38
Logique temporelle
Logique Temporelle Linéaire (LTL)

Sémantique (4/ 4)
On considère une formule LTL φ sur Σ. On dit qu’un mot infini u ∈ ∑ω satisfait φ à la position i
,noté
(i ∈ N * ) quand :

• , s’il existe j ≥ 0 tel que :

✓ ,

✓ Pour tout 0 ≤ k < j,

Exemple :

39
Logique temporelle
Logique Temporelle Linéaire (LTL)

Exemple explicatif
On considère :

40
Logique temporelle
Logique Temporelle Linéaire (LTL)

Exemple explicatif
On considère :

41
Logique temporelle
Logique Temporelle Linéaire (LTL)

Exemple explicatif
On considère :

42
Logique temporelle
Logique Temporelle Linéaire (LTL)

Exercice d’application
On considère :

? 43
Logique temporelle
Logique Temporelle Linéaire (LTL)

Exercice d’application
On considère :

 oui

 oui

 oui 44
Logique temporelle
Logique Temporelle Linéaire (LTL)

Exercice d’application
On considère :

? ?

? 45
Logique temporelle
Logique Temporelle Linéaire (LTL)

Exercice d’application
On considère :

 oui  non

 oui avec j = 2

 oui avec j = 0 46
Logique temporelle
Logique Temporelle Linéaire (LTL)

Sémantique (suite)

Exemple :

47
Logique temporelle
Logique Temporelle Linéaire (LTL)

Opérateurs

48