Universite de Yaounde 1

GENIE LOGICIEL
INF4027

Model CHECKING

Groupe 8

Examinateur : Pr. ATSA Etoundi

Roger
Année académique : 2023-2024
Membres du groupe :

Fomubad Borista Fondi 20V2001

Fouda Jean Bosco 19M2425
Fouotsop Fosso Patrick 20U2585
Kaldadak Adama 20U2836
Kenfack Ngahou Jaurès 20U2883
Kongne Mbouhom Anderson Luther 18X2309
Leuna Fienkak Nkeheup 20U2698
Mengue Essomba Agnès Mileine 18T2764
Tomdieu Tchadieuko Ivan Gottfried 20U2947
Ngainsu Kamsu Hans Celim Jaures 20U2612
Table des matières
I Vue d’ensemble 2

II Objectifs 2

III Introduction 3

IV Pourquoi le modèle checking ? 3

V Principes fondamentaux de vérification de modèles 4

V.1 Modélisation du système . . . . . . . . . . . . . . . . . 4
V.2 Propriétés à Vérifier (Spécifications) . . . . . . . . . . . 5
V.2.1 Représentation des propositions en logique Tem-
porelle . . . . . . . . . . . . . . . . . . . . . . . 6
V.2.2 Catégories de propriétés d’un système . . . . . . 6

VI Domaines d’application du modèle checking 7

VII Outils et techniques 7

VII.1Outils . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
VII.2Techniques . . . . . . . . . . . . . . . . . . . . . . . . . 8
VII.2.1 Techniques d’abastractions . . . . . . . . . . . . 8
VII.2.2 Techniques de réduction . . . . . . . . . . . . . 9

VIII
. Limites du model checking 9
VIII.1 Explosion d’état et algorithmes symboliques . . . . . 9
VIII.2. Spécification incorrectes . . . . . . . . . . . . . . . . . 10

IX Exemple 10
IX.1 L’exemple du four à micro-ondes . . . . . . . . . . . . 10
IX.1.1 Modèle . . . . . . . . . . . . . . . . . . . . . . . 11
IX.1.2 Spécifications . . . . . . . . . . . . . . . . . . . 11
IX.1.3 Vérification . . . . . . . . . . . . . . . . . . . . 14
I Vue d’ensemble
Le model checking, ou vérification de modèle, est une approche for-
melle utilisée dans le domaine de la conception et de la vérification
des systèmes informatiques et matériels. À un niveau général, le model
checking consiste à examiner de manière exhaustive toutes les tra-
jectoires possibles d’un système afin de garantir que celui-ci satisfait
certaines propriétés spécifiées. La vérification est généralement faite de
manière automatique. Sur le plan pratique, la vérification de modèles
est devenue, au niveau industriel, la méthode de vérification de code et
de systèmes matériels la plus populaire et la plus utilisée aujourd’hui
car offre une assurance rigoureuse quant à la correction d’un système,
en identifiant et en éliminant les erreurs potentielles avant même son
déploiement.

II Objectifs
1. Initiation à la recherche : Il s’agit d’une étape cruciale dans
notre développement académique et professionnel. Que ce soit
dans le cadre universitaire, d’un projet professionnel, ou d’une
exploration personnelle.
2. Application de la vérification de modèle : Comprendre la notion
de vérification de modèles, ses enjeux et pouvoir l’appliquer sur
des modèles concrets de notre entourage

2
III Introduction
.La vérification de modèles s’appuie sur la logique temporelle en
informatique. Le model checking commence avec les travaux d’Edmund
M. Clarke, E. Allen Emerson, Jean Pierre Queille et Joseph Sifakis au
tout début des années 1980. Clarke, Emerson et Sifakis se sont vu
attribuer le prix Turing 2007 pour leurs travaux sur le model checking.

IV Pourquoi le modèle checking ?

Le model checking est né de la nécessité de développer des méthodes
formelles de vérification pour garantir la fiabilité et la correction des
systèmes informatiques et matériels. Plusieurs facteurs ont contribué
à l’émergence et à l’adoption du model checking dans le domaine de la
recherche en informatique et en ingénierie :
1. Complexité croissante des systèmes : Avec l’augmentation de
la complexité des systèmes informatiques et matériels, il est
devenu de plus en plus difficile d’assurer leur fiabilité et leur
correction par des méthodes de test traditionnelles.
2. Exigences critiques dans certaines applications : Certains do-
maines, tels que l’aérospatiale, les systèmes embarqués, les réseaux
de communication et les systèmes de contrôle industriel, exigent
des niveaux élevés de fiabilité et de sécurité.

3
 Figure 1 – Processus du modèle checking

V Principes fondamentaux de vérification

de modèles
V.1 Modélisation du système
Avant d’appliquer la vérification de modèles, il est essentiel de
modéliser le système sous forme d’un modèle mathématique. Les modèles
les plus couramment utilisés sont les automates, les réseaux de Pétri,
et les diagrammes d’états. Le système est modélisé par un système de
transition d’états généralement. Il s’agit d’un graphe orienté : un som-
met représente un état du système et chaque arc représente une tran-
sition, c’est-à-dire une évolution possible du système d’un état donné
vers un autre état. Chaque état du graphe orienté est étiqueté par l’en-
semble des propositions atomiques vraies à ce point d’exécution (par
exemple, i=2, le processeur 3 est en attente, etc.). Un tel graphe est

4
 Figure 2 – Exemple : Modèle d’un distributeur de boisson

aussi appelé une [stucture de kripke] Structure de Kripke.

V.2 Propriétés à Vérifier (Spécifications)

La [logique temporelle]logique temporelle est un langage formel
utilisé pour exprimer des propriétés de systèmes qui évoluent dans le
temps. Elle nous permet de raisonner sur des propositions qualifiées
en termes de temps (par exemple, ”J’ai toujours faim”, ”Je finirai par
avoir faim”, ”Je serai affamé jusqu’à ce que je mange quelque chose”).
Deux logiques temporelles couramment utilisées dans la vérification de
modèles sont la Logique Temporelle Linéaire (LTL) et la Logique de
l’Arbre de Calcul ou CTL (computation tree logique).
LTL est utilisée pour exprimer des propriétés qui se maintiennent
sur une séquence infinie d’états, tandis que CTL est utilisée pour ex-
primer des propriétés qui se maintiennent sur différentes branches d’un
arbre de calcul. Les formules LTL utilisent généralement des opérateurs
tels que ”next” (X), ”eventually” (F), ”always” (G) et ”until” (U), tan-
dis que les formules CTL utilisent des opérateurs tels que ”existential”
(E), ”universal” (A), ”next” (X), ”until” (U) et ”finally” (F).

5
V.2.1 Représentation des propositions en logique Tempo-
relle
Quelques exemples de propositions en LTL includent :
1. ”La voiture accélère jusqu’à atteindre une vitesse de 100 km/h”
peut être représenté comme ”acceleration U (speed = 100 km/h)”.
2. ”La température finira par atteindre 40 degrés Celsius” peut
être représenté comme ”F(temperature = 40 degrés Celsius)”.
3. ”La température finira par atteindre 40 degrés Celsius” peut
être représenté comme ”F(temperature = 40 degrés Celsius)”.
Un exemple de proposition en CTL :
1. ”Le signal d’accord doit toujours être activé à un moment donné
après que le signal de demande ait été activé.” AG (demande −→
AF accord)

V.2.2 Catégories de propriétés d’un système

On distingue deux catégories de propriétés dans un systèmes :
1. Les propriétés de sûreté (safety) garantissant l’absence d’états
indésirables comme ≪ l’ascenseur bouge toujours avec les portes
fermées ≫
2. Les propriétés de vivacité (liveness) garantissant qu’un état sou-
haité est éventuellement atteint comme ≪ si l’ascenseur est ap-
pelé à un certain étage, alors il ira à cet étage ≫.

6
VI Domaines d’application du modèle che-
cking
1. Systèmes Embarqués : La vérification de modèles est largement
utilisée dans le domaine des systèmes embarqués pour garantir
la fiabilité des logiciels critiques, tels que ceux utilisés dans les
avions, les voitures autonomes, et les dispositifs médicaux.
2. Protocoles de Communication : Elle est également appliquée à
la vérification des protocoles de communication pour s’assurer
qu’ils respectent des propriétés telles que la non-violation de la
confidentialité et la sécurité.
3. Systèmes Distribués : Les systèmes distribués complexes, tels
que les réseaux de capteurs et les applications cloud, bénéficient
de la vérification de modèles pour garantir leur robustesse et leur
cohérence.

VII Outils et techniques

VII.1 Outils
Des outils tels que [model checking tools] SPIN, NuSMV, et
PRISM sont largement utilisés pour la vérification de modèles. Ces
logiciels permettent de spécifier le système, les propriétés à vérifier, et
exécutent l’analyse automatiquement.
1. SPIN (Simple Promela Interpreter) : est un outil général pour
vérifier la correction de modèles logiciels concurrents de manière
rigoureuse et généralement automatisée. Il a été écrit, à partir de
1980, par Gerard J. Holzmann et d’autres membres du groupe
Unix du Computing Sciences Research Center des Bell Labs.
Le logiciel est disponible gratuitement depuis 1991 et continue
d’évoluer pour suivre le rythme des nouveaux développements

7
 dans ce domaine. Les systèmes à vérifier sont décrits en langage
Promela (abréviation pour Process Meta Language)
2. NuSMV : est une ré implémentation et une extension du vérificateur
de modèle symbolique SMV , le premier outil de vérification de
modèle basé sur des diagrammes de décision binaires L’outil a
été conçu comme une architecture ouverte pour la vérification
de modèles. Il vise à vérifier de manière fiable les conceptions
de taille industrielle, à utiliser comme backend pour d’autres
outils de vérification et comme outil de recherche pour les tech-
niques de vérification formelle. NuSMV a été développé dans
le cadre d’un projet conjoint entre l’ITC-IRST ( Istituto tren-
tino di cultura à Trente ), l’Université Carnegie Mellon , l’Uni-
versité de Gênes et l’ Université de Trente et prend en charge
l’analyse des spécifications exprimées en CTL (structure arbo-
rescente dans laquelle l’avenir n’est pas déterminé) et LTL (Lo-
gique Temporelle linéaire) . Il peut être exécuté en mode batch
ou de manière interactive avec une interface utilisateur textuelle.

VII.2 Techniques
En raison de la complexité souvent exponentielle des modèles, des
techniques d’abstraction et de réduction sont appliquées pour rendre
l’analyse plus faisable sans sacrifier la précision.

VII.2.1 Techniques d’abastractions

1. Suppression de Détails : Omission de détails non essentiels du
modèle tout en maintenant les caractéristiques cruciales pour la
vérification.
2. Approximation de Comportement : Utilisation de modèles moins
complexes qui préservent néanmoins des caractéristiques com-
portementales essentielles.

8
 3. Modélisation hiérarchique : Structuration du modèle en niveaux
hiérarchiques pour simplifier l’analyse.

VII.2.2 Techniques de réduction

1. Techniques Symboliques : Représentation symbolique des états
pour réduire la complexité de l’exploration.
2. Agrégation d’États : Regroupement d’États similaires pour réduire
la taille de l’espace d’État.
3. Compression d’État : Réduction du nombre d’états en identi-
fiant et éliminant les états redondants qui n’apportent pas d’in-
formations supplémentaires à la vérification. Cette technique est
souvent basée sur la détection de cycles dans l’espace d’états.

VIII . Limites du model checking

VIII.1 Explosion d’état et algorithmes symbo-
liques
Pour vérifier un modèle, un outil de vérification de modèle reçoit
un modèle abstrait dans un formalisme donné (par exemple, une struc-
ture de Kripke) et la spécification du modèle en logique temporelle, puis
analyse le comportement du modèle en explorant de manière exhaus-
tive son espace d’états. [state space] L’espace d’états fait référence à
l’ensemble de tous les états possibles dans lesquels un système peut se
trouver pendant son exécution. Il englobe toutes les combinaisons pos-
sibles de valeurs pour les variables d’état du système. À mesure que le
nombre d’états d’un système augmente, son espace d’états augmente
considérablement, ce qui entraı̂ne une explosion d’état.
L’explosion d’état est l’augmentation exponentielle de l’espace d’états
à mesure que le nombre de variables d’état dans un système augmente.
Cela a un impact direct sur la complexité de la vérification du modèle.

9
Pour résoudre le problème de l’explosion d’état, nous utilisons une
technique de vérification de modèle appelée algorithme symbolique.
Les algorithmes symboliques abordent le problème de l’explosion
d’état en travaillant sur une représentation compacte de l’espace d’états
du système au lieu d’énumérer explicitement tous les états individuels,
ce qui permet une exploration plus efficace des grands espaces d’états.
Ces algorithmes manipulent des formules symboliques qui représentent
des ensembles d’états et les propriétés du système, ce qui permet une
exploration plus efficace des grands espaces d’états. En utilisant un
algorithme symbolique, l’outil de vérification de modèle peut mani-
puler efficacement les formules symboliques représentant les états et
les propriétés. Il effectue des opérations telles que la conjonction, la
disjonction et la quantification sur ces formules, sans énumérer expli-
citement chaque état individuel.

VIII.2 . Spécification incorrectes

La garantie de la correction dépend fortement de la qualité de la
spécification du système. Une spécification incorrecte peut conduire à
des résultats de vérification erronés.

IX Exemple
IX.1 L’exemple du four à micro-ondes
Spécification informelle du fonctionnement d’un four à micro-ondes :
Pour cuire dans le four, ouvrez la porte, placez la nourriture à l’intérieur
et refermez la porte. Ne mettez pas de récipients en métal dans le four.
Appuyez sur le bouton de démarrage. Le four se réchauffera pendant
30 secondes, puis commencera la cuisson. Lorsque la cuisson est ter-
minée, le four s’arrêtera. Le four s’arrêtera également si la porte est
ouverte pendant la cuisson. Si le four est démarré alors que la porte

10
est ouverte, une erreur se produira et le four ne chauffera pas. Dans
ce cas, le bouton de réinitialisation peut être utilisé. Nous utilisons le
vérificateur de modèle [NuSVM] NuSVM pour effectuer la vérification
du modèle de ce système.

IX.1.1 Modèle
Nous modélisons le système du four à micro-ondes en fonction de la
description donnée. Le résultat est un graphe orienté où chaque transi-
tion représente les actions se déroulant dans le système (par exemple,
ouvrir ou fermer la porte du four, démarrer le four et le réchauffement
du four). Le comportement du four est suivi à l’aide des variables d’état
Start, Closed, Heat et Error. La figure ci-dessous illustre la structure
de Kripke résultante du système du four à micro-ondes.

IX.1.2 Spécifications
Nous donnons les spécifications pour le modèle en suivant la des-
cription du système du four à micro-ondes.
1. Si le four chauffe, alors la porte est fermée : AG(Heat −→
Closed)
2. Chaque fois que le bouton de démarrage est enfoncé, éventuellement
le four se réchauffera :
AG(Start −→ AF Heat)
3. Chaque fois que le four est correctement démarré, éventuellement
le four se réchauffera :
AG((Start ∧ ¬Error) −→ AF Heat)
4. Chaque fois qu’une erreur se produit, il sera toujours possible
de cuisiner :
AG(Error −→ EF Heat)

11
Figure 3 – structure de Kripke du système du four à micro-ondes

12
Figure 4 – Modèle du système de four à micro-ondes en langage
NuSMV

13
Figure 5 – Spécifications du système de four à micro-ondes en NuSMV

IX.1.3 Vérification
Pour vérifier le modèle, nous exécutons le fichier source avec la com-
mande NuSMV. À l’exécution, le résultat est un affichage qui indique
si toutes les spécifications sont vraies ou un contre-exemple indiquant
un modèle incorrect ou une formalisation de spécification incorrecte.
La Figure 5 montre le résultat lorsque nous exécutons la commande
NuSMV sur le four à micro-ondes. Le code complet pour la vérification
du système de four à micro-ondes se trouve dans le dépôt Github.

14
Figure 6 – Résultat de la vérification (sortie de la commande
NuSMV)

15
Références
[1] wikipedia Kripke structure
[2] Sanjit A. Seshia, EECS 294-98: Introduction to Temporal Logic
[3] Wikipedia: model checking tools
[4] Edmund M. Clarke1, William Klieber1, Milos Novacek2, and Paolo
Zuliani1: Model Checking and the State Explosion Problem
[5] NuSMV: a new symbolic model checker

16