Programmation Synchrone
Systèmes Temps Réel
Vérification formelle de
programme Lustre
Ouassila Labbani-Narsis
3
[email protected] Problématique
Pour développer un système, il faut …
❑ savoir analyser et comprendre le
problème,
❑ savoir proposer une solution à ce problème,
❑ savoir utiliser les bons
outils et savoir implanter
la solution
❑ Savoir analyser et vérifier la
solution 2
Problématique
« A l’origine de toute erreur attribuée
à l’ordinateur, vous trouverez au
moins deux erreurs humaines. Dont
celle consistant à attribuer l’erreur à
l’ordinateur. »
Vérification au plus haut
niveau
Plus une erreur est détectée tard dans le cycle
de développement, plus elle est coûteuse à
corriger
4
Vérification au plus haut
niveau
5
Vérification au plus haut
niveau
6
Vérification au plus haut
niveau
7
Vérification au plus haut
niveau
8
Vérification au plus haut
niveau
9
Vérification au plus haut
niveau
10
Objectifs de la vérification
❑ Eviter les bugs
❑ Assurer la qualité
❑ Réduire le coût
Validation et vérification
Validation – Principe générale
Le système est-il conforme au cahier des charges ?
Objectif : détecter les non conformités ➔ Tests
Test - Limites
« Tester, c’est très long… »
« Pas complétement
automatique… »
Vérification – Principe générale
Le système vérifie-t-il la propriété ?
Techniques de vérification formelle
Objectif : prouver la correction
Qu’est-ce qu’une Technique
Formelle?
❑L’ambition initiale des techniques formelles : supprimer
les phases de tests lors de la conception des programmes
❑Tests coûteux en temps et donc en... argent
❑Tests fastidieux pour le développeur...
❑Le test n’est jamais exhaustif : il ne peut pas vérifier toutes
les exécutions possibles du système...
❑L’utilisation des techniques formelles ne peux remplacer
totalement les activités de tests
❑On travaille sur un modèle du système : c’est une
abstraction et l’on ne travaille donc pas sur le monde réel...
Qu’est-ce qu’une Technique
Formelle?
Tests Vs Techniques Formelles
17
Qu’est-ce qu’une Technique
Formelle?
Tests Vs Techniques Formelles
18
Qu’est-ce qu’une Technique
Formelle?
Exemple
19
Qu’est-ce qu’une Technique
Formelle?
Exemple
20
Qu’est-ce qu’une Technique
Formelle?
Exemple
21
Qu’est-ce qu’une Technique
Formelle?
Exemple
22
Qu’est-ce qu’une Technique
Formelle?
Technique Formelle : définition rigoureuse
⚫ Le système de preuve permet la démonstration des propriétés
relevantes du système
⚫ Il travaille sur un modèle du système
⚫ La preuve sur programme permet de s’assurer que le modèle que
nous avons réalisé se comporte de la bonne façon, c’est à dire
qu’il vérifie des propriétés exigées, qu’il n’a pas de bugs, …
23
Classification des Techniques
Formelles suivant la sémantique
Deux types de spécifications formelles
1. Approche basée sur modèles ou approche constructive,
opérationnelle, basée sur état explicite :
Se fonde sur une sémantique à états (Automates...)
L’état est modifié par les opérations
Les opérations modélisent l’aspect comportemental du système
Les propriétés sont exprimées par des expressions logiques sur les
variables du système
STE, Réseaux de Petri, B...
2. Approche algébrique ou fonctionnelle :
Sémantique définie par une algèbre
Variables et opérations sont définies suivant cette algèbre
Le système est décrit par un ensemble d’équations
Ensemble d’équations = description du comportement
LOTOS, LUSTRE..
24
Systèmes de preuves en
informatique
Deux techniques de preuves sur modèle :
1. Theorem Proving (TP) ou vérification par preuves :
Utilisation d’une axiomatique et d’un système de déduction
logique
Preuve = Théorème du système axiomatique considéré
Exemple de Theorem prover : B, PVS, Coq ...
2. Model-Checking (MC) ou vérification exhaustive :
Basée sur une description du système sous forme d’automate
Vérification d’une propriété par parcours exhaustif des états
du système → propriétés vrai quelques soit l’exécution du
système
Exemple de Model-Checker : SPIN, VDM ...
25
Principe du model-checking
26
Principe du model-checking
27
Principe du model-checking
28
Principe du model-checking
29
Principe du model-checking
⚫ L’automate explicite est un modèle des
comportements possibles du programme
⚫ Explorer l’automate = étudier les propriétés
du programme
⚫ Problème : l’automate est généralement
infini (ou énorme)) impossible de l’explorer
⚫ Idée : travailler sur une abstraction finie (et
pas trop grosse) de l’automate
⚫ Cette abstraction doit conserver certaines
propriétés du programme
30
Vérification de programme Lustre
⚫ Les méthodes de vérification s’appliquent à tout
langage/formalisme basé sur une notion de
temps discret
➔ Lustre et les autres langages synchrones, et bien
d’autres ...
Notion de propriété temporelle
⚫ On s’intéresse aux propriétés fonctionnelles
⚫ Le programme calcule-t-il les bonnes sorties en
fonction de ses entrées ?
⚫ Une propriété = une relation entre les séquences
d’entrées et de sorties
⚫ On parle de propriété temporelle
31
Vérification de programme Lustre
Sûreté et vivacité
⚫ Il existe toute une théorie sur les propriétés (et
les logiques) temporelles
⚫ On retiendra simplement une définition “intuitive”
de la partition classique entre :
Sûreté (safety) : quelque chose (de mauvais) n’arrive
jamais
Vivacité (liveness) : quelque chose (de bon) finit par
arriver
⚫ Distinction importante car :
Les safety sont de simples invariants, elles permettent
de raisonner sur des séquences arbitrairement longues
Les liveness font référence à un futur non borné, elles
nécessitent de raisonner sur des séquences infinies
32
Vérification de programme Lustre
De quoi a-t-on besoin?
Pour faire de la vérification formelle, il faut :
1. Un modèle du programme compréhensible par le
prouveur utilisé
Ici modèle Lustre = modèle exprimable sous forme d’automate
2. Un prouveur pour vérifier les propriétés logiques
On utilise ici le Model Checker Lesar
3. Une logique pour décrire les propriétés à prouver
On utilise ici la logique temporelle Safety Logic (exprimable en
Lustre)
4. Des assertions pour décrire les hypothèses sous
lesquels on raisonne 33
Vérification de programme Lustre
Lustre permet l’expression de comportements
attendus … puis leur vérification
⚫ Cohérence du programme (analyse statique) : avant la
compilation
⚫ Seuls les comportements attendus équivalents à des
propriétés de sûreté peuvent être exprimés et vérifiés
(«une situation indésirable ne peut pas se produire»)
⚫ Analyse exhaustive de l’espace d’états du programme
Le système n’entre pas dans un ensemble d’états mauvais
⚫ Vérification par introduction d’observateurs
Utilisation de clauses assert / signaux de sortie
Un module concurrent observant l’évolution de certains flots
⚫ Analyse par simulation
34
Vérification de programme Lustre
⚫ Des assertions permettent de tenir compte de l’environnement
du programme en exprimant des contraintes sur ses entrées en
fonction de ses sorties
⚫ Une assertion est une formule logique sur les flots d’entrée et de
sortie, qui doit être toujours vraie
➔ Permet de restreindre l’espace d’exploration
⚫ Introduction d’un module observateur pour démontrer une
propriété
Permet de vérifier que Pg satisfait Phi sous l’hypothèse que ses
entrées et ses sorties satisfont l’assertion H
H B’
(Assertion)
Pg O
I Programme à
vérifier Phi B
Propriété à
démontrer
Pg_Phi 35
Vérification par assertion
Permet au concepteur d'expliciter les hypothèses
faites sur l'environnement et/ou sur le programme
lui-même
➔ Permet d'optimiser la compilation
➔ Permet la vérification de propriétés sous conditions
➔ Simplifie la conception des programmes
Exemple :
assert (not (X and Y))
affirme que les flots booléens X et Y ne doivent jamais être
vrais simultanément
assert (true -> not (X and pre(X)))
affirme que le flot booléen X ne transporte jamais deux
valeurs vraies consécutives
36
Justin, le loup, la chèvre
et le chou…
⚫ Justin veut traverser une
rivière avec
un loup
une chèvre
un chou
⚫ Mais…
seul Justin peut manœuvrer la barque
la barque ne contient que deux places (Justin + loup, ou
Justin + chèvre, ou Justin + chou)
en l'absence de Justin, la chèvre mange le chou
en l'absence de Justin, le loup mange la chèvre
➔ description de ce système multi agents en Lustre37
Justin, le loup, la chèvre
et le chou…
⚫ Les entrées du programmes : les actions de Justin
m : Justin traverse la rivière seul
mw : Justin traverse la rivière avec le loup
mg : Justin traverse la rivière avec la chèvre
mc : Justin traverse la rivière avec le chou
➔ flots booléens
bn = vrai signifie que l'action b est effectuée à l'instant n
bn = faux signifie que l'action b n'est pas effectuée à
l'instant n
⚫ Hypothèse : les actions sont instantanées
38
Justin, le loup, la chèvre
et le chou…
⚫ Les sorties du programmes :
J : position de Justin
W : position du loup
G : position de la chèvre
C : position du chou
➔ flots entiers à valeurs dans {0, 1, 2}
Xn = 0 signifie que X est sur la rive 0 à l'instant n
Xn = 1 signifie que X est sur la rive 1 à l'instant n
Xn = 2 signifie que X a été mangé à l'instant n
39
Justin, le loup, la chèvre
et le chou…
node justin(m, mw, mg, mc : bool) returns (J, W, G, C : int);
assert(m or mw or mg or mc);
assert(not (m and mw));
assert(not (m and mg));
assert(not (m and mc));
assert(not (mw and mg));
assert(not (mw and mc));
assert(not (mg and mc));
assert(true -> not (mw and not (pre(J)=pre(W))));
assert(true -> not (mg and not (pre(J)=pre(G))));
assert(true -> not (mc and not (pre(J)=pre(C))));
let
J = 0 -> 1 - pre(J);
W = 0 -> if mw then 1 - pre(W) else pre(W);
G = 0 -> if pre(G) = 2 then pre(G) else if mg then 1 - pre(G)
else if (pre(G)=pre(W) and not mw)
then 2 else pre(G);
C = 0 -> if pre(C) = 2 then pre(C) else if mc then 1 - pre(C)
else if (pre(C)=pre(G) and not mg)
then 2 else pre(C);
tel 40
Justin, le loup, la chèvre
...
et le chou…
J = 0 -> 1 - pre(J);
W = 0 -> if mw then 1 - pre(W) else pre(W);
G = 0 -> if pre(G) = 2 then pre(G) else if mg then 1 - pre(G)
else if (pre(G)=pre(W) and not mw)
then 2 else pre(G);
C = 0 -> if pre(C) = 2 then pre(C) else if mc then 1 - pre(C)
else if (pre(C)=pre(G) and not mg)
then 2 else pre(C);
...
Quelle est la séquence d’actions gagnante ?
41
Justin, le loup, la chèvre
...
et le chou…
J = 0 -> 1 - pre(J);
W = 0 -> if mw then 1 - pre(W) else pre(W);
G = 0 -> if pre(G) = 2 then pre(G) else if mg then 1 - pre(G)
else if (pre(G)=pre(W) and not mw)
then 2 else pre(G);
C = 0 -> if pre(C) = 2 then pre(C) else if mc then 1 - pre(C)
else if (pre(C)=pre(G) and not mg)
then 2 else pre(C);
...
0 1 2 3 4 5 6 7
Séquence d'actions gagnante : mg m mc mg mw m mg
J 0 1 0 1 0 1 0 1
mg, m, mc, mg, mw, m, mg
W 0 0 0 0 0 1 1 1
G 0 1 1 1 0 0 0 1
C 0 0 0 1 1 1 1 1
42
Vérification par module concurrent
Principe :
⚫ Expression des propriétés attendues sous la forme de
nœud LUSTRE retournant un flot booléen
⚫ Composition de ce nœud avec le programme à vérifier
⚫ Examen de l’automate obtenu
Outils :
⚫ Permet la vérification de programmes mettant en
œuvre des flots booléens et des flots numériques
définis par des relations linéaires
⚫ LESAR et NP-tools (intégré dans l’outil SCADE)
43
Vérification par module concurrent
Pg O observateur
Programme à
I
vérifier
Phi
Propriété à B
démontrer
Pg_Phi
⚫ Pg = programme à vérifier écrit en LUSTRE
⚫ Phi = observateur (propriété à démontrer écrite en LUSTRE)
➔ Pg_Phi = Pg || Phi (programme écrit en LUSTRE)
Phi est satisfaite ssi tous les états de Pg_Phi sont
étiquetés par la valeur true sur le flot B
➔ Vérification de Pg = génération du système de transitions
correspondant à Pg_Phi et test des valeurs prises par B dans
chaque état
44
Vérification par module concurrent
Observateur :
Programme qui calcule un (et un seul) flot booléen
en fonction de ses entrées (de type quelconque)
➔ permet de modéliser des propriétés fonctionnelles
attendues
Exemple :
node never (A : bool) returns (B : bool);
let
B = not A -> not A and pre(B);
tel
➔ never(X) est vrai tant que X est faux
45
Vérification de programme Lustre
Exemple :
Soit la propriété attendue suivante
« toute occurrence de A doit être suivie par une occurrence de B
avant la prochaine occurrence de C »
Peut être exprimée au passé par
« à chaque occurrence de C, il faut que A ne se soit jamais
produit, ou si A s’est produit, il faut que B se soit produit depuis
la dernière occurrence de A »
Exprimable en LUSTRE par le nœud
node once_B_from_A_to_C (A,B,C:bool) returns (X:bool);
let
X = C -> (never(A) or since(B,A));
tel
node since (X,Y:bool) returns (Z:bool)
let
Z = if Y then X else (true -> X or pre(Z));
tel
46
Lustre + Lesar =
Technique formelle
⚫ Lustre est un langage à syntaxe et sémantique
formelle :
Syntaxe rigoureuse ➔ les constructions du langages ne
possèdent qu’une interprétation possible
Sémantique à base mathématique : sémantique fonctionnelle
à base de flots de données
⚫ LESAR est l’ outil de preuve associé à Lustre : preuve
par Model Checking
47
Notion d’automate : rappel
⚫ Un automate est un graphe orienté permettant de
décrire l’ensemble des états possibles d’un système
ainsi que son comportement dynamique
⚫ Un programme Lustre définie un automate fini car
son espace mémoire est borné (Pas d’allocations
dynamiques)
⚫ Dans un programme Lustre, l’ensemble des états
représente l’ensemble des combinaisons de valeurs
possibles des variables du programme 48
Programme Lustre = automate
Exemple passage code Lustre → automate
node notE(E :bool) returns(S :bool);
let
S = not E ;
tel
49
Programme Lustre = automate
Exemple passage code Lustre → automate
node notE(E :bool) returns(S :bool);
let
S = not E ;
tel
50
SL : Safety Logic
⚫ En vérification formelle Lustre, la logique permettant
de décrire les formules à vérifier est exprimable en
langage Lustre
⚫ Il s’agit de la logique temporelle SL pour Safety Logic
Remarque : Il existe des logiques temporelles plus
expressives (CTL,LTL, ...) permettant d’exprimer des
propriétés plus complexe : propriétés de vivacité,
d’équité, atteignabilité, ...
51
Expression des propriétés à
prouver
Une propriété Lustre sera donc
exprimée par un noeud définissant une
relation logique entre :
des flots d’entrées de types bool
et un unique flot de sortie de type bool
➔ Notion d’observateur
52
Exemple complet : le
chronomètre STOP_WATCH
Cahier des charges
Le but est de spécifier le comportement d’un
chronomètre simplifié. Le chronomètre dispose de 3
entrées de trois boutons :
On_off : permet d’activer et de désactiver le
chronomètre;
reset : remet le chronomètre à zéro quand le
chronomètre est désactivé;
freeze : gèle ou dégèle l’affichage quand le
chronomètre est actif
Prototype du noeud :
node STOPWATCH(on_off, reset, freeze : bool)
returns (time : int );
53
Exemple complet : le
chronomètre STOP_WATCH
Travail préliminaire : l’opérateur COUNT
⚫ Prototype du nœud COUNT :
node COUNT(reset,X : bool) returns (C : int);
⚫ Spécification :
Remise à 0 si reset, sinon il est incrémenter si X;
Tout se passe comme si C valait 0 à l’origine
54
Exemple complet : le
chronomètre STOP_WATCH
Travail préliminaire : l’opérateur COUNT
55
Exemple complet : le
chronomètre STOP_WATCH
Travail préliminaire : l’opérateur COUNT
node COUNT(reset, X : bool)
returns (C : int) ;
let
C = if reset
then 0
else if X
then 0 −> pre(C) + 1
else 0 −> pre(C) ;
tel
56
Exemple complet : le
chronomètre STOP_WATCH
Travail préliminaire : l’opérateur SWITCH
⚫ Prototype du nœud SWITCH :
node SWITCH(on,off : bool)returns (S : bool);
⚫ Spécification :
Passe de False à True si on;
Passe de True à False si off ;
Tout se comporte comme si S était False à l’origine ;
Doit fonctionner correctement même si off et on sont les
mêmes
⚫ Hypothèses sur l’environnement extérieur :
On et off ne sont jamais à True deux fois de suite... Cette
hypothèse simule un appui court sur un interrupteur, par
exemple... 57
Exemple complet : le
chronomètre STOP_WATCH
Travail préliminaire : l’opérateur SWITCH
58
Exemple complet : le
chronomètre STOP_WATCH
Travail préliminaire : l’opérateur SWITCH
node SWITCH ( on, off : bool )
returns ( S : bool ) ;
assert( not(on and pre(on)) )
assert( not(off and pre(off)) )
let
S = if (false -> pre(S))
then not off
else on ;
tel
59
Exemple complet : le
chronomètre STOP_WATCH
Description du nœud STOP_ SWITCH
node STOP_WATCH (on_off, reset, freeze : bool)
returns (time : int) ;
assert(true -> not(on_off and pre(on_off)))
assert(true -> not(reset and pre(reset)))
assert(true -> not(freeze and pre(freeze)))
var running, freezed : bool , cpt : int ;
let
running = SWITCH (on_off, on_off) ;
freezed = SWITCH( freeze and running,
freeze or on_off) ;
cpt = count( reset and not running, running) ;
time = if freezed
then ( 0 -> pre(time))
else cpt ;
tel 60
Exemple complet : le
chronomètre STOP_WATCH
Exécution du nœud STOP_ SWITCH
61
Exemple complet : le
chronomètre STOP_WATCH
Vérification du nœud STOP_ SWITCH
Nous cherchons à vérifier la propriété de sûreté suivante :“ Il n’est
pas possible de remettre à zéro le compteur en cours d’exécution”
➔ Pour cela, nous ajouterons une hypothèse supplémentaire au
nœud principal :
assert(on_off = true -> false)
Idée : Le chronomètre est activé à l’instant initial et reste en
exécution jusqu’à la fin...
Nous construisons le noeud permettant d’observer cette propriété :
node observateur_prop(on_off, reset, freeze : bool,
S : int) returns (P : bool)
let
P = true -> if (S=0) then false else pre(P) ;
tel
62
Exemple complet : le
chronomètre STOP_WATCH
Vérification du nœud STOP_ SWITCH
Nous construisons ensuite le noeud de vérification :
node VERIF(on_off,reset,freeze : bool)
returns (B : bool) ;
let
B = observateur_prop(on_off, reset, freeze,
STOP_WATCH(on_off, reset, freeze)) ;
tel
Il n’y a plus qu’à lancer le noeud VERIF dans le
prouveur LESAR
63
Exemple du compteur de balises
⚫ Un train circule sur une voie :
Il croise des balises, disposées sur la voie
Il reçoit un signal : seconde
Vitesse idéale : 1 balise/seconde
⚫ Compteur de balises embarqué :
Décide si on est à l’heure, en avance ou en retard
Utilise une hystérésis pour éviter les oscillations d’état
(décalage des conditions de changement d’état)
➔ Hystérésis = retard de l’effet sur la cause,
la propriété d’un système qui tend à
demeurer dans un certain état quand la
cause extérieure qui a produit le
changement d’état à cessé
➔ Oscillation = mouvement périodique
répétitif 64
Exemple du compteur de balises
node compteur(sec,bal: bool)
returns (alheure,retard,avance: bool);
var diff : int;
let
diff = (0 -> pre diff) +
(if bal then 1 else 0) +
(if sec then -1 else 0);
avance = (true -> pre alheure) and (diff > 3)
or (false -> pre avance) and (diff > 1);
retard = (true -> pre alheure) and (diff < -3)
or (false -> pre retard) and (diff < -1);
alheure = not (avance or retard);
tel
65
Exemple du compteur de balises
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
sec F F F F V F V V V F F F V V V V V V V V
bal V V V V F V F F F V V V F F F F F F F F
alheure V V V F F F F F V V V F F F V V V V V F
retard F F F F F F F F F F F F F F F F F F F V
avance F F F V V V V V F F F V V V F F F F F F
Méthodes Formelles 66
Exemple du compteur de balises
Quelques propriétés en Lustre :
⚫ On ne peut pas être en avance et en retard :
ok = not (avance and retard);
⚫ On ne peut pas passer directement d’en retard à en
avance :
ok = true -> not ((pre retard) and avance);
⚫ On ne peut pas rester en retard pendant un seul
instant :
ok = ((not PPretard) and Pretard) => retard;
avec :
Pretard = false -> pre retard;
PPretard = false -> pre Pretard;
67
Remarques …
1. La propriété :
« Si le train stoppe, il finira par être en retard »
est une liveness, elle ne peut pas être vérifiée
en utilisant le model checker Lesar
2. L'outil de vérification LESAR est un model checker
capable de vérifier si la propriété est vérifiée
quelque soit l'état du noeud.
On utilise la commande :
lesar mon_fichier.lus Pg_Phi
68
L’outil graphique xLesar
xLesar : une interface graphique du vérificateur Lesar
69
Notre objectif …
Apprendre à concevoir et à vérifier un
logiciel embarqué critique …
70
Quel avenir ? https://www.systerel.fr/
Quel avenir ? https://www.ansys.com/fr-fr/
Quel avenir ? https://www.ansys.com/fr-fr/
Quel avenir ? https://www.elsys-design.com/fr/
Quel avenir ? https://www.aerocontact.com/
Quel avenir ? https://www.apec.fr/
