Cours "G nie Logiciel II"
Partie2: M thodes formelles pour la
sp cification et la v rification de
sp cification et la v rification de
logiciels
Niveau: II2
Enseignante: Rim DRIRA
AU: 2017/2018
1
Objectifs du cours
o Introduire la sp cification et la v rification
formelle dans la d marche de d veloppement
dun logiciel
o Apprendre une m thode formelle: la m thode
B
o Apprendre deux techniques de v rification
formelle
n Preuve de th or mes
n V rification de mod les ou model checking
2
Plan
o Chapitre1: Introduction aux m thodes
formelles
o Chapitre2: La m thode B AMN
(Abstract Machine Notation)
o Chapitre3: V rification de mod les (ou
model checking)
3
Pr -requis
o G nie Logiciel 1
o Logiques formelles (propositions, pr dicats,
interpr tation, Syst mes formels, axiomes, th or mes)
o Th orie des langages (automates finis et composition)
o Th orie des langages (automates finis et composition)
4
R f rences
o J.-R. Abrial, The B book, Cambridge University Press, 1996.
o , Modeling in Event-B : System and Software Engineering, Cambridge
University Press, 2010.
o : Fr d ric Gervais , "Combinaison de sp cifications formelles pour la
mod lisation des syst mes dinformation , th se de doctorat, Universit de
Sherbrooke, 2006.
http://cedric.cnam.fr/fichiers/RC1103.pdf
o : Jacques Julliand, cours "Sp cification, V rification et Test" , Universit
Franche-comt , 2008.
http://lifc.univ-fcomte.fr/~julliand/Lecon1_A_8SVT.pdf
o : Olfa Mosbahi, "D veloppement formel des syst mes automatis s ,
o : Olfa Mosbahi, "D veloppement formel des syst mes automatis s ,
th se de doctorat, Universit Tunis-ElManar, 2008.
http://pegase.scd.inpl-nancy.fr/theses/2008_MOSBAHI_O.pdf
o H.P. Nguyen, "D rivation de sp cifications formelles B partir de
sp cifications semi-formelles", Th se de Doctorat, CNAM, France, 1998.
http://lacl.univ-paris12.fr/laleau/sourcePublis/Before2003/PHD-PHNguyen.pdf
o : Ian Sommerville, "Le G nie Logiciel , Addison-Wesley, 1992.
(biblioth que de lENSI)
5
R f rences
Autres R f rences Bibliographiques
o David Harel, Michal Politi, Modeling reactive systems with statecharts
the statemateapproach, McGraw-Hill, 1998,
o Zohar Manna, Amir Pnueili, The Temporal Logic of Reactive and
Concurrent Systems: Specification, Springer, 1992.
Concurrent Systems: Specification, Springer, 1992.
o Kevin Lano, The B language and method: a guide to practical formal
development, Springer, 1996,
o Philippe Schnoebelen, V rification de logiciels Techniques et outils du
model-checking, Vuibert, 1999.
o Christel Baier, Joost-Pieter Katoen, Principles of Model-Checking, MIT
Press Cambridge, London, 2008.
6
Introduction
o Plusieurs cat gories de syst mes
d velopper
n Les syst mes grande consommation
o Exemples: jeux, familiale, financi re, etc.
n Les syst mes sur mesure
o Exemples: gestion de stock,
o Les syst mes automatis s s rs de
Les syst mes automatis s s rs de
fonctionnement
n Exemples: Robots pour r aliser des t ches
p nibles dans lindustrie, distributeur de
boisson, feu de croisement, acc s un parking
payant, a ronautiques, etc.
Ces syst mes exigent un niveau de
s ret et de fiabilit lev
7
Pourquoi l'approche formelle?
o Validation difficile r aliser: montrer que le logiciel
r pond sa sp cification.
o V rification limit e (coh rence entre les tapes du
d veloppement) et non automatis e
o Impossibilit de garantir labsence derreurs: Non
exhaustivit des cas envisag s lors des tests
o Co t lev de la correction des erreurs surtout quand
elles sont d tect es tard dans le cycle de d veloppement.
8
Co t dune erreur 1/2
oPlus les erreurs sont d tect es tard dans le cycle de
d veloppement, plus les co ts de correction sont lev s.
> 1000 heures / erreur
Maintenance
100 heures / erreur
Validation Finale
Installation sur site
Fin du d veloppement
Fin du d veloppement
10 heures / erreur
Tests dInt gration
1 heure / erreur
Tests Unitaire
Fin de leffort de d veloppement
En cas
derreur
D veloppement du code
source
9
Co t dune erreur 2/2
o En phase de validation
n L quipe de d veloppement nest plus disponible
n Linstallation est report e
o En phase dinstallation
n Le produit ne fonctionne pas correctement
perte du service
n Le produit ne fonctionne pas du tout
perte de la mission
n Le produit cause des atteintes la vie humaine
Atteinte limage de lentreprise et perte financi re
Les cons quences sont donc plus catastrophiques pour
les syst mes automatis s qui exigent une s ret de
fonctionnement
10
Que faire alors ?
o Le d veloppement classique des syst mes automatis s s rs de
fonctionnement n cessite des tests qui peuvent la fin obliger
le d veloppeur refaire le d veloppement.
o Lutilisation des m thodes formelles permet de rem dier ce
probl me. En effet ce sont des m thodes bas es sur un
fondement math matique offrant la pr cision, labsence
fondement math matique offrant la pr cision, labsence
dambiguit &..
o On peut ainsi partir des besoins sp cifi s au d part, d velopper
un mod le formel pour ce syst me (d crivant laspect
comportemental, fonctionnel et structurel), exprimer
formellement les exigences et effectuer la preuve.
11
Publicité
Que faire alors ?
Le Syst me
satisfait-il des exigences
Technique S mantique
Mod le
Dautomates
Ou bien
Ou bien
Technique Syntaxique
Formules Logiques
?
|==
?
|--
Formule logique
Formule logique
Il faut quon arrive, apr s ce cours,
Il faut quon arrive, apr s ce cours,
mod liser, formaliser et v rifier
mod liser, formaliser et v rifier
12
Chapitre1: Introduction aux m thodes
formelles
Objectifs
n Sensibiliser lint r t dintroduire les m thodes
formelles dans le cycle de d veloppement dun
logiciel
n Comprendre comment on peut introduire les
m thodes formelles dans le cycle de d veloppement
m thodes formelles dans le cycle de d veloppement
dun logiciel
n D finir les termes cl s dans le domaine des m thodes
formelles
n Pr senter quelques formalismes de sp cification
formelle
n Introduire les techniques de la v rification formelle
13
Chapitre1: Introduction la sp cification et la
v rification formelles
Plan
1. Syst mes automatis s s rs de
fonctionnement
2. N cessit des m thodes formelles
3. M thodes formelles et cycle de
3. M thodes formelles et cycle de
d veloppement
4. Comportement, environnement,
propri t s
5. Techniques de V rification
14
Syst mes automatis s s rs de
fonctionnement
fonctionnement
15
Syst mes automatis s s rs de
fonctionnement
o Un syst me est dit automatis sil ex cute
toujours le m me cycle de travail pour
lequel il a t programm
o Les syst mes automatis s s rs de
fonctionnement exigent un niveau de
fonctionnement exigent un niveau de
s ret et de fiabilit lev
o Ce sont des syst mes qui doivent r pondre
dans toutes les ex cutions possibles aux
propri t s exig es par lutilisateur
16
Syst mes automatis s s rs de
fonctionnement
Quelque chose de
mauvais narrivera
jamais
Quelque chose de
bien arrivera
n cessairement
Propri t s de s ret
Propri t s de vivacit
Commandes
Syst me
physique
Syst me
Informatique
de commandes
Informations sur l tat du
syst me physique
17
Exemple dun passage niveau
o Le syst me physique est la barri re
o Le composant de contr le (le syst me informatique
d velopper) agit sur la barri re pour quelle soit baiss e
ou relev e
o Une propri t attendue de ce syst me (s ret ): Le
syst me ne doit pas permettre un acc s simultan au
syst me ne doit pas permettre un acc s simultan au
trafic ferroviaire et au trafic routier
Le passage niveau
18
Exemple dun syst me de contr le dun
chauffage
Le syst me informatique est un syst me de contr le dun
chauffage
La propri t de s ret est li e la temp rature ambiante
qui ne doit pas d border dun intervalle.
Lenvironnement est la temp rature.
Le composant physique (command ) est lappareil de
chauffe
chauffe
Le contr leur (qui est le logiciel que nous avons
d velopper) re oit en entr e la valeur de la temp rature et
agit sur le composant physique si n cessaire pour chauffer
ou refroidir
Le composant logique (le contr leur) et le composant
physique ( contr l ) doivent se comporter de fa on ce que
la propri t soit v rifi e (temp rature dans un intervalle).
19
Autres exemples
Le distributeur de billets
Les robots
Les feux de carrefour
La barri re de parking
20
Syst mes automatis s s rs de
fonctionnement
o Pour r duire la complexit et assurer un bon
fonctionnement, lutilisation des m thodes formelles
appara t comme une solution principale
o Elle consiste Introduire la sp cification et la
v rification formelles dans le cycle de d veloppement
dun logiciel
o Le syst me est ainsi sp cifi et v rifi avant quil
ne soit impl ment
o Le document de r f rence devient le document formel
labor par la sp cification
21
M thodes formelles
22
Bref historique
o Avant dans les ann es 70, lutilisation des m thodes formelles se
r alisait apr s limpl mentation
n Le programme est traduit en automate et la v rification se fait sur
lautomate.
n Cependant, la correction dune erreur d couverte ce stade tait
tr s couteuse.
o Avec la complexit du code, les d veloppeurs ont pens introduire la
o Avec la complexit du code, les d veloppeurs ont pens introduire la
v rification dans une phase tr s avanc e du cycle de d veloppement.
o Les logiques (propositionnelles et de pr dicats) n taient pas
Publicité
suffisantes pour d crire un comportement. On a pens introduire les
logiques temporelles.
o Avec l volution des bases de donn es, la th orie des ensembles et la
th orie des fonctions ont t introduites dans les approches formelles
dans les ann es 90.
23
M thodes Formelles
o Les m thodes formelles consistent utiliser
les math matiques pour le d veloppement
de logiciels.
o Les principales activit s sont :
n l criture dune sp cification formelle ;
n l criture dune sp cification formelle ;
n la v rification formelle de la sp cification
laide de raisonnements math matiques.
o Corriger la sp cification si besoin
n la construction de programmes en transformant
formellement la sp cification.
24
Sp cification formelle: D finition
o Une sp cification dun logiciel est formelle si elle est
exprim e avec un langage qui poss de:
o un vocabulaire et une syntaxe formellement d finis;
o une s mantique bas e sur les math matiques.
o Expression dans un langage formel du quoi dun syst me
d velopper
d velopper
o Offre une description claire, pr cise et non ambigu du
syst me sans r f rence aux d tails d'impl mentation:
n La mod lisation du fonctionnement du syst me.
n La formulation rigoureuse des propri t s attendues du
syst me
25
Sp cification formelle
o Avantages :
n Rigueur et pr cision des sp cifications
o Faciliter la validation
n Automatiser la v rification
n Pr venir les erreurs
o Inconv nients :
o Inconv nients :
n N cessite une certaine qualification du client,
utilisateurs et d veloppeurs
n Difficult de communication
26
Comparaison
Sp cifications semi-formelles
Sp cifications formelles
J Mod les graphiques et
intuitifs,
J Support de
communication
J Editeurs visuels
J Editeurs visuels
L Absence dune
s mantique pr cise,
L Pas de v rification de
propri t s (s ret ,
vivacit , etc.)
J S mantique pr cise et
rigoureuse
J Possibilit dautomatisation
de la v rification de
de la v rification de
propri t s
J Faciliter la validation
L Difficiles utiliser par les
non familiaris s
L Manque de support de
communication
Voir pour des d tails sur les possibilit s de d river des
sp cifications formelles partir de sp cifications semi-formelles
27
Transformation formelle
o Processus
qui
commence
par
l laboration
dune
sp cification formelle du syst me
o Et qui se poursuit en transformant cette sp cification par
sp cification
parvenir
raffinement
suffisamment raffin e pour donner un code ex cutable.
jusqu
une
o Permet s'investir dans les points les plus fins par tapes
et d composer la v rification.
28
V rification formelle
o Prouver formellement des propri t s sur le
syst me d s sa sp cification
o Lors dune transformation formelle:
n Prouver les propri t s
n Prouver les propri t s
n Prouver le passage dun mod le un autre
o Par d finition, la v rification est "la
confirmation de preuves que les exigences
sp cifi es ont t satisfaites" (ISO 8402).
29
M thodes formelles et cycle
de d veloppement
de d veloppement
30
M thodes formelles et cycle de
d veloppement
o Introduire une phase de
sp cification formelle
n Le document de r f rence devient le
document formel labor par la
sp cification
sp cification
o Int grer la v rification formelle
dans les d marches de conception de
logiciels.
n Le syst me est ainsi sp cifi et v rifi
avant quil soit impl ment
31
M thodes formelles et cycle de
d veloppement
Validation
Analyse
des besoins
Exigences: propri t s
attendues (ex: de s ret )
Sp cification
formelle
Conception
Conception
Codage
Tests
Exploitation /
Maintenance
V rification
32
Sp cification formelle et validation 1/2
o La validation consiste se demander si le texte
formel traduit le cahier des charges
o La sp cification formelle permet de poser les
bonnes questions et d tre plus rigoureux
bonnes questions et d tre plus rigoureux
La validation est facilit e
o La validation ne peut pas tre automatis e
33
Publicité
Sp cification formelle et validation 2/3
o Lors du passage du cahier des charges vers la
Sp cification formelle, on risque toujours de:
n Mal interpr ter les besoins
n Ne pas pouvoir formaliser toutes les propri t s qui
couvrent la totalit des besoins.
Quelques voies pour viter ces probl mes:
Quelques voies pour viter ces probl mes:
n Compl ter la v rification formelle par de la validation
partir de jeux de tests,
n Utiliser plusieurs langages formels pour
augmenter le pouvoir d'expression et combiner
l'efficacit des m thodes de v rification
34
M thodes formelles et cycle de
d veloppement
o Les m thodes formelles ne sont
pas limit es la sp cification
mais couvent aussi:
n Conception: par transformation formelle
on passe de la sp cification du pseudo-
on passe de la sp cification du pseudo-
code
n Codage: on peut g n rer
automatiquement du code ex cutable
n Preuve: On prouve chaque tape le
respect des sp cifications initiales
35
Formalismes pour repr senter
des sp cifications
o les langages d riv s de la logique classique pour
exprimer des syst mes transformationnels,
o les logiques temporelles pour exprimer des propri t s
dynamiques de vivacit des syst mes r actifs,
o les langages logico-ensemblistes comme Z, VDM et B
pour d crire et v rifier des propri t s statiques sur les
tats des syst mes,
tats des syst mes,
o les r seaux de Petri,
les automates communicants,
LOTOS pour mod liser des syst mes concurrents avec
ou sans partage de variables,
o les automates temporis s pour mod liser des syst mes
temps r els
36
Mod lisation des
exigences: Propri t s
exigences: Propri t s
attendues
37
Types de propri t s
o S ret (Safety) Invariants
n Quelque chose de mauvais narrivera
jamais
o pas dacc s simultan de A et B la
section critique
o Vivacit (Liveness)
Vivacit (Liveness)
n Quelque chose de bien arrivera
n cessairement
o si A veut entrer la section, alors
in vitablement il aura cet acc s
38
Types de propri t s
Fatalit
sous
n nonce que,
conditions
quelque chose de bien finira par avoir lieu
au moins une fois partir dun certain tat.
n Dans ce cas, on se situe dans la classe des
n Dans ce cas, on se situe dans la classe des
certaines
propri t s de vivacit .
Equit
n nonce que, sous certaines conditions,
quelque chose aura lieu un nombre infini
de fois.
39
Types de propri t s
Atteignabilit
o Ces
propri t s
noncent
quune
certaine situation peut tre atteinte.
o Nous pouvons exprimer aussi que
quelque chose nest jamais atteignable
quelque chose nest jamais atteignable
alors
et
dinatteignabilit .
n Dans ce cas, on se situe dans la classe des
parlons
nous
propri t s de s ret .
40
Exemple : Contr leur de feux de circulation
dun carrefour
o Probl me: sp cifier le fonctionnement dun
contr leur de feux tricolores dun carrefour.
o Les feux peuvent tre :
n Hors service (hs) : tous les feux sont au jaune
n En service (es) : ils voluent selon
n En service (es) : ils voluent selon
vert
rouge
jaune
rouge
n Lorsque le feu est au rouge sur une voie, les
v hicules de cette voie ne peuvent sengager
dans le carrefour
41
Exemple : Contr leur de feux de circulation
dun carrefour
o Propri t s souhait es:
n Condition de s ret (safety) : les
v hicules ne peuvent sengager dans les
deux voies simultan ment.
n Condition de vivacit (liveness) : les
n Condition de vivacit (liveness) : les
v hicules ne sont pas bloqu s infiniment
sur lune des (ou les deux) voies.
o Ces propri t s sont d crites par :
((feuA=rouge) (feuB rouge)) ((feuA rouge) (feuB=rouge))
42
Exemple: Acc s une section critique
Etant donn e une section critique (SC), un
algorithme dexclusion mutuelle doit satisfaire :
1- exclusion mutuelle (EM) suret : si un processus
est en SC alors aucun processus ne peut y tre.
2- progr s (P) vivacit : si un groupe de processus
demande dentrer en SC alors lun deux doit
demande dentrer en SC alors lun deux doit
obtenir lacc s
3- equite (E) vivacit : tout processus demandant
dentrer en SC doit y entrer ( au bout dun certain
temps) pas de famine
43
Techniques de
v rification
v rification
44
Techniques de v rification
Deux approches de v rification:
o Preuve de th or mes (v rification
syntaxique)
Publicité
o V rification de mod les ou model
o V rification de mod les ou model
checking (v rification s mantique)
45
Techniques de v rification
Preuve
n consiste prouver des propri t s partir
des axiomes du syst me et dun
ensemble de r gles dinf rence.
n tr s puissantes
n tr s puissantes
n elles traitent des syst mes nombre
d' tats infinis
n elles sont ind cidables dans le cas
g n ral,
F difficiles automatiser.
46
Techniques de v rification
Model checking
n permet de savoir si un automate donn v rifie une
formule temporelle donn e
n consiste parcourir exhaustivement lespace d etats
dun mod le fini du syst me v rifier.
n Les propri t s v rifier sont g n ralement
n Les propri t s v rifier sont g n ralement
exprim es en logique temporelle.
n Un contre exemple est g n r lorsque la propri t
nest pas v rifi e par le mod le consid r .
n enti rement automatiques
n limit es aux syst mes ayant un nombre fini d' tats
F posent des probl mes en temps de traitement et en
espace m moire li s l'explosion combinatoire en
nombre d' tats.
47
Techniques de v rification
Principe simplifi du model-checking
48
Une pr cision: TEST vs Preuve
oUn test qui m ne une ex cution
incorrecte apporte une information
mais un test correct napporte aucune
information
oUne preuve correcte permet dindiquer
quune propri t P est v rifi e, alors
que limpossibilit de faire une preuve
ne renseigne pas sur lanomalie
49
Comparaison
Preuve
Model checking
J Applicable aux syst mes
nombre infini d' tats
L Difficult d'automatiser les
preuves de propri t s
dynamiques
dynamiques
L En cas d' chec de la preuve
automatique, l'utilisateur doit
d terminer si c'est une erreur
ou une difficult de preuve.
L Lutilisateur doit guider le
prouveur.
J Simple utiliser
J Automatisation de la
v rification des propri t s
dynamiques
dynamiques
L Limit par l'explosion
combinatoire du graphe
d' tat (probl me de place
m moire et de temps de
calcul).
L Limit aux automates
nombre fini d' tats.
50
Mod liser et v rifier
selon la classe de
selon la classe de
syst mes
51
Mod liser et v rifier selon la classe de
syst mes
o les langages formels et les outils associ s sont
adapt s certaines classes de probl mes et
pas d'autres.
o Sp cifier et v rifier selon la classe dun
syst me:
n Syst mes finis et syst mes infinis
n Syst mes transformationnels et
syst mes r actifs
52
Mod liser et v rifier selon la classe de
syst mes
Syst mes finis= syst mes nombre fini
d' tats: une classe o la question de la
v rification est en g n ral d cidable.
Syst mes infinis = syst mes nombre infini
Syst mes infinis = syst mes nombre infini
d' tats o la question de la v rification est, en
g n ral, ind cidable.
53
Mod liser et v rifier selon la classe de
syst mes
Syst mes transformationnels
o Syst me transformationnel : retourne des r sultats
partir de donn es. Le syst me est totalement sourd
aux changements de son environnement.
o Exemples: un compilateur, un solveur de
syst mes d' quations lin aires, etc.
o
54
Mod liser et v rifier selon la classe de
syst mes
Syst mes r actifs
o Un syst me r actif est un syst me qui volue dans
un environnement dont il doit prendre en compte
les volutions pendant son fonctionnement.
n Il interagit constamment avec son environnement en
recevant des stimuli et en retournant des
commandes.
commandes.
o Exemples: un syst me d'exploitation, un IHM,
un Protocole de communication, etc.
55
Mod liser et v rifier selon la classe de
syst mes
Sp cifier et v rifier un syst me transformationnel
o Une sp cification bo te noire par une pr et une post
condition d crivant les tats initiaux et finaux du
syst me, convient.
o les langages d riv s de la logique classique
permettent de mod liser et v rifier des syst mes
transformationnels.
transformationnels.
Sp cifier et v rifier un syst me r actif
o Sp cification bo te de verre du syst me et de son
environnement.
o On sp cifie une collection dactions et des propri t s sur
leurs encha nements dans les comportements internes
du syst me.
o les logiques temporelles permettent de mod liser et
v rifier les propri t s dynamiques des syst mes r actifs.
56