Cours Génie Logiciel II: Méthodes formelles pour la spécification et la vérification de logiciels

? |--

Formule logique

Formule logique

Il faut qu’on arrive, après ce cours, à Il faut qu’on 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  Sensibiliser à l’intérêt d’introduire les méthodes formelles dans le cycle de développement d’un logiciel

 Comprendre comment on peut introduire les

méthodes formelles dans le cycle de développement méthodes formelles dans le cycle de développement d’un logiciel

 Définir les termes clés dans le domaine des méthodes

formelles

 Présenter quelques formalismes de spécification

formelle

 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

 Un système est dit automatisé s’il exécute toujours le même cycle de travail pour lequel il a été programmé

 Les systèmes automatisés sûrs de

fonctionnement exigent un niveau de fonctionnement exigent un niveau de sûreté et de fiabilité élevé

 Ce sont des systèmes qui doivent répondre dans toutes les exécutions possibles aux propriétés exigées par l’utilisateur

16

Systèmes automatisés sûrs de

fonctionnement

Quelque chose de mauvais n’arrivera 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 d’un passage à niveau

 Le système physique est la barrière

 Le composant de contrôle (le système informatique à

développer) agit sur la barrière pour qu’elle soit baissée ou relevée

 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 d’un système de contrôle d’un chauffage

Le système informatique est un système de contrôle d’un chauffage La propriété de sûreté est liée à la température ambiante qui ne doit pas déborder d’un intervalle. L’environnement est la température. Le composant physique (commandé) est l’appareil 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

 Pour réduire la complexité et assurer un bon

fonctionnement, l’utilisation des méthodes formelles apparaît comme une solution principale

 Elle consiste à Introduire la spécification et la

vérification formelles dans le cycle de développement d’un logiciel

 Le système est ainsi spécifié et vérifié avant qu’il

ne soit implémenté

 Le document de référence devient le document formel

élaboré par la spécification

21

Méthodes formelles

22

Bref historique

 Avant dans les années 70, l’utilisation des méthodes formelles se

réalisait après l’implémentation  Le programme est traduit en automate et la vérification se fait sur

l’automate.

 Cependant, la correction d’une erreur découverte à ce stade était

très couteuse.

 Avec la complexité du code, les développeurs ont pensé à introduire la  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.

 Les logiques (propositionnelles et de prédicats) n’étaient pas

suffisantes pour décrire un comportement. On a pensé à introduire les logiques temporelles.

 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

 Les méthodes formelles consistent à utiliser les mathématiques pour le développement de logiciels.

 Les principales activités sont :

 l’écriture d’une spécification formelle ;  l’écriture d’une spécification formelle ;  la vérification formelle de la spécification à

l’aide de raisonnements mathématiques.  Corriger la spécification si besoin

 la construction de programmes en transformant

formellement la spécification.

24

Spécification formelle: Définition

 Une spécification d’un logiciel est formelle si elle est

exprimée avec un langage qui possède:

 un vocabulaire et une syntaxe formellement définis;  une sémantique basée sur les mathématiques.  Expression dans un langage formel du quoi d’un système à

développer développer

 Offre une description claire, précise et non ambiguë du système sans référence aux détails d'implémentation:  La modélisation du fonctionnement du système.  La formulation rigoureuse des propriétés attendues du

système

25

Spécification formelle

 Avantages :

 Rigueur et précision des spécifications

 Faciliter la validation  Automatiser la vérification  Prévenir les erreurs

 Inconvénients :  Inconvénients :

 Nécessite une certaine qualification du client,

utilisateurs et développeurs  Difficulté de communication

26

Comparaison

Spécifications semi-formelles

Spécifications formelles

 Modèles graphiques et

intuitifs,  Support de

communication

 Editeurs visuels  Editeurs visuels  Absence d’une

sémantique précise,

 Pas de vérification de propriétés (sûreté, vivacité, etc.)

 Sémantique précise et

rigoureuse

 Possibilité d’automatisation

de la vérification de de la vérification de propriétés

 Faciliter la validation  Difficiles à utiliser par les

non familiarisés

 Manque de support de

communication

Voir [Ngu98] pour des détails sur les possibilités de dériver des spécifications formelles à partir de spécifications semi-formelles

27

Transformation formelle

 Processus

qui

commence

par

l’élaboration

d’une

spécification formelle du système

 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

à

 Permet s'investir dans les points les plus fins par étapes

et décomposer la vérification.

28

Vérification formelle

 Prouver formellement des propriétés sur le

système dès sa spécification

 Lors d’une transformation formelle:

 Prouver les propriétés  Prouver les propriétés  Prouver le passage d’un modèle à un autre

 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

 Introduire une phase de spécification formelle  Le document de référence devient le

document formel élaboré par la spécification spécification

 Intégrer la vérification formelle

dans les démarches de conception de logiciels.  Le système est ainsi spécifié et vérifié

avant qu’il 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

 La validation consiste à se demander si le texte

formel traduit le cahier des charges

 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

 La validation ne peut pas être automatisée

33

Spécification formelle et validation 2/3

 Lors du passage du cahier des charges vers la Spécification formelle, on risque toujours de:  Mal interpréter les besoins  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:

 Compléter la vérification formelle par de la validation

à partir de jeux de tests,

 Utiliser plusieurs langages formels pour

augmenter le pouvoir d'expression et combiner l'efficacité des méthodes de vérification [Ger06]

34

Méthodes formelles et cycle de développement

 Les méthodes formelles ne sont pas limitées à la spécification mais couvent aussi:  Conception: par transformation formelle on passe de la spécification à du pseudo- on passe de la spécification à du pseudo- code

 Codage: on peut générer

automatiquement du code exécutable  Preuve: On prouve à chaque étape le

respect des spécifications initiales

35

Formalismes pour représenter des spécifications

 les langages dérivés de la logique classique pour

exprimer des systèmes transformationnels,

 les logiques temporelles pour exprimer des propriétés

dynamiques de vivacité des systèmes réactifs,

 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,  les réseaux de Petri,

les automates communicants, LOTOS pour modéliser des systèmes concurrents avec ou sans partage de variables,

 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

 Sûreté (Safety) Invariants

 Quelque chose de mauvais n’arrivera

jamais  pas d’accès simultané de A et B à la

section critique  Vivacité (Liveness) Vivacité (Liveness)  Quelque chose de bien arrivera

nécessairement  si A veut entrer à la section, alors inévitablement il aura cet accès

38

Types de propriétés

Fatalité

sous

 Énonce que,

conditions quelque chose de bien finira par avoir lieu au moins une fois à partir d’un certain état.  Dans ce cas, on se situe dans la classe des  Dans ce cas, on se situe dans la classe des

certaines

propriétés de vivacité.

Equité

 Énonce que, sous certaines conditions, quelque chose aura lieu un nombre infini de fois.

39

Types de propriétés

Atteignabilité  Ces

propriétés

énoncent

qu’une

certaine situation peut être atteinte.  Nous pouvons exprimer aussi que quelque chose n’est jamais atteignable quelque chose n’est jamais atteignable alors et d’inatteignabilité.  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 d’un carrefour

 Problème: spécifier le fonctionnement d’un contrôleur de feux tricolores d’un carrefour.

 Les feux peuvent être :

 Hors service (hs) : tous les feux sont au jaune  En service (es) : ils évoluent selon  En service (es) : ils évoluent selon vert

rouge

jaune

rouge

 Lorsque le feu est au rouge sur une voie, les véhicules de cette voie ne peuvent s’engager dans le carrefour

41

Exemple : Contrôleur de feux de circulation d’un carrefour

 Propriétés souhaitées:

 Condition de sûreté (safety) : les

véhicules ne peuvent s’engager dans les deux voies simultanément.

 Condition de vivacité (liveness) : les  Condition de vivacité (liveness) : les véhicules ne sont pas bloqués infiniment sur l’une des (ou les deux) voies.  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 d’exclusion 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 d’entrer en SC alors l’un d’eux doit demande d’entrer en SC alors l’un d’eux doit obtenir l’accès 3- equite (E) vivacité : tout processus demandant d’entrer en SC doit y entrer ( au bout d’un certain temps) – pas de famine

43

Techniques de vérification vérification

44

Techniques de vérification

Deux approches de vérification:  Preuve de théorèmes (vérification

syntaxique)

 Vérification de modèles ou model  Vérification de modèles ou model checking (vérification sémantique)

45

Techniques de vérification

Preuve

 consiste à prouver des propriétés à partir

des axiomes du système et d’un ensemble de règles d’inférence.

 très puissantes  très puissantes  elles traitent des systèmes à nombre

d'états infinis

 elles sont indécidables dans le cas

général,  difficiles à automatiser.

46

Techniques de vérification

Model checking

 permet de savoir si un automate donné vérifie une

formule temporelle donnée

 consiste à parcourir exhaustivement l’espace d’´etats

d’un modèle fini du système à vérifier.  Les propriétés à vérifier sont généralement  Les propriétés à vérifier sont généralement

exprimées en logique temporelle.

 Un contre exemple est généré lorsque la propriété

n’est pas vérifiée par le modèle considéré.

 entièrement automatiques  limitées aux systèmes ayant un nombre fini d'états

 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

Un test qui mène à une exécution

incorrecte apporte une information mais un test correct n’apporte aucune information

Une preuve correcte permet d’indiquer qu’une propriété P est vérifiée, alors que l’impossibilité de faire une preuve ne renseigne pas sur l’anomalie

49

Comparaison

Preuve

Model checking

 Applicable aux systèmes à

nombre infini d'états

 Difficulté d'automatiser les preuves de propriétés dynamiques dynamiques

 En cas d'échec de la preuve

automatique, l'utilisateur doit déterminer si c'est une erreur ou une difficulté de preuve.

 L’utilisateur doit guider le

prouveur.

 Simple à utiliser  Automatisation de la

vérification des propriétés dynamiques dynamiques

 Limité par l'explosion

combinatoire du graphe d'état (problème de place mémoire et de temps de calcul).

 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

 les langages formels et les outils associés sont adaptés à certaines classes de problèmes et pas à d'autres.

 Spécifier et vérifier selon la classe d’un

système:  Systèmes finis et systèmes infinis  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  Système transformationnel : retourne des résultats à partir de données. Le système est totalement sourd aux changements de son environnement.

 Exemples: un compilateur, un solveur de

systèmes d'équations linéaires, etc.



54

Modéliser et vérifier selon la classe de

systèmes

Systèmes réactifs  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.  Il interagit constamment avec son environnement en

recevant des stimuli et en retournant des commandes. commandes.

 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

 Une spécification boîte noire par une pré et une post condition décrivant les états initiaux et finaux du système, convient.

 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

 Spécification boîte de verre du système et de son

environnement.

 On spécifie une collection d’actions et des propriétés sur leurs enchaînements dans les comportements internes du système.

 les logiques temporelles permettent de modéliser et vérifier les propriétés dynamiques des systèmes réactifs.

56