Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Introduction aux méthodes formelles

Module Développement Logiciel : Approche Formelle & à
Objets

Pascal ANDRE

MIAGE
Université de Nantes

Master Miage M1

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Plan
Introduction

Motivations

Un exemple introductif

Les systèmes formels

La spécification formelle

Une classification des méthodes formelles

Exemples

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Rappel du contexte

Contexte de l’intervention 1/2

Le contexte
1. Génie logiciel
2. Le développement du logiciel
3. Méthode de développement du logiciel
I Modèles, produits
I Processus
I Validation, vérification
4. Qualité

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Rappel du contexte

Contexte de l’intervention 2/2

I De l’idée au code
I exprimer
I programmer → MODELES
I vérifier
I avec méthode.
I dans le bon ordre PROCESSUS
I éviter l’anarchie → GESTION DE PROJET
I travailler en groupe
I et qualité
I modèles (correct, fiable, évolutif...)
I processus (efficace, rentable...) → QUALITE

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Position de la Miage et références

Introduction : méthodes formelles en Miage

1. Master MIAGe M1 Nantes
I Le développement du logiciel
I Les méthodes formelles : application à Z
I Les méthodes à objets : du formel avec OCL
2. Master MIAGe M2 Nantes (Parcours IRSI)
I B (BTool)
I Algèbres de processus (LOTOS)

Vers un usage rationnel

I bonnes pratiques de spécification (précision)
I bonnes pratiques de conception (assertions, preuves)
I bonnes pratiques de programmation (tests)
I bonnes pratiques du processus (rigueur)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Position de la Miage et références

Introduction : méthodes formelles en Miage

Quelques références
I Développement du logiciel et CSI [AV01a, GMSB96]
I Systèmes formels [Lau86, WL88]
I Z [Spi94, WL88], B [Abr96]
I Méthodes formelles et Z
[Mey92, BH96, Bow96, Jac97, AV01b, AV04]
I LOTOS, SDL [Tur93], CSP [Hoa85] ou CCS [Mil89]
I Spécifications algériques [Wir90]
I Automates [Arn92], les réseaux de PETRI [Bra83])

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Position de la Miage et références

Jean-Raymond Abrial.
Spécifier ou comment matérialiser l’abstrait.
Technique et Science Informatique, 3(3):201–219, 1984.

Jean-Raymond Abrial.
The B-Book Assigning Programs to Meanings.
Cambridge University Press, 1996.
ISBN 0-521-49619-5.
André Arnold.
Systèmes de transitions finis et sémantique des processus communiquants.
Collection Etudes et recherches en informatique. Masson, 1992.
ISBN 2-225-82746-X.
Pascal André and Alain Vailly.
Conception de systèmes d’information ; Panorama des méthodes et des techniques,
volume 1 of Collection Technosup.
Editions Ellipses, 2001.
ISBN 2-7298-0479-X.
Pascal André and Alain Vailly.
Spécification des logiciels ; Deux exemples de pratiques récentes : Z et UML,
volume 2 of Collection Technosup.
Editions Ellipses, 2001.
Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Position de la Miage et références

ISBN 2-7298-0774-8.
Pascal André and Alain Vailly.
Exercices corrigés en langage Z ; Les spécifications formelles par la pratique,
volume 4 of Collection Technosup.
Editions Ellipses, 2004.
ISBN 2-7298-1942-8.
Jonathan P. Bowen and Michael G. Hinchey, editors.
Applications of Formal Methods.
International Series in Computer Science. Prentice-Hall, 1 edition, 1996.
ISBN 0-13-832544-8.
Jonathan Bowen.
Formal Specification & Documentation using Z: A Case Study Approach.
International Thomson Publishing, 1996.
ISBN 1-85032-230-9.
G. W. Brams.
Réseaux de Petri : théorie et pratique.
Editions Masson, Paris, 1983.
Marie-Claude Gaudel, Bruno Marre, Françoise Schlienger, and Gilles Bernot.
Précis de génie logiciel.
Enseignement. Masson, 1996.
Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Position de la Miage et références

ISBN 2-225-85189-1.
Charles Antony Richard Hoare.
Communicating Sequential Processes.
International Series in Computer Science. Prentice-Hall, 1985.
ISBN 0-13-153289-8.
Jonathan Jacky.
The Way of Z: Practical Programming with Formal Methods.
Cambridge University Press, 1997.
ISBN 0-521-55041-6.
Cliff B Jones.
VDM, une méthode rigoureuse pour le développement du logiciel.
Masson, Paris, 2e edition, 1993.
Jean.-Louis Laurière.
Résolution de problèmes par l’Homme et la machine.
Eyrolles, 1986.
Bertrand Meyer.
Introduction to the Theory of Programming Languages.
International Series in Computer Science. Prentice Hall, 1992.
ISBN 0-13-498502-8.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Position de la Miage et références

Robin Milner.
Communication and Concurrency.
International Series in Computer Science. Prentice-Hall, 1989.
ISBN 0-13-115007-3.
Mike Spivey.
La notation Z.
Collection Méthodologies du logiciel. Editions Masson, 1994.
Traduit de l’anglais par Michel Lemoine, ISBN 2-225-84367-8.
Kenneth J. Turner, editor.
Using Formal Description Techniques, An introduction to Estelle, Lotos and
SDL.
Wiley, 1993.
ISBN 0-471-93455-0.
Jeannette M. Wing.
A specifier’s introduction to formal methods.
IEEE Computer, 23(9):8–24, 1990.

Martin Wirsing.
Algebraic Specification, volume B of
Handbook of Theoretical Computer Science, chapter 13, pages 675–788.
Elsevier, 1990.
Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Jan Van Leeuwen, Editor.

J. Woodcock and M. Loomes.
Software Engineering Mathematics.
Addison Wesley, 1988.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Plan
Introduction

Motivations

Un exemple introductif

Les systèmes formels

La spécification formelle

Une classification des méthodes formelles

Exemples

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Chiffres et besoins

Quelques chiffres sur le GL

I abandon logiciels : 2/6 (de grande taille)
I retard > 50% durée prévue livraison logiciels : 75%
I qualité = problématique coûteuse (60% des coûts totaux -
Gardner)
I coût bugs & erreurs des logiciels
I 59.5 MM$ par an, économie EU (estimation NIST 2002)
I 175 MM$ en 2002 entreprises US (estimation NRC 2002) pour
réparer les dommages causés par des logiciels défectueux
I (quelques) catastrophes :
I Therac 25, ’85-’87 : 6 patients irradiés, 2 morts
I Syst. Bagages Aéroport Denver, ’95 : 16mois, 3.2 Mds$
I Ariane 5 - vol 88/501, ’96: 40s de vol, destr., 850 M$
I Mars Climate Orbiter & Mars Polar Lander, ’99 : destr.

Source: P. Poizat, Borland

Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Chiffres et besoins

Bugs et qualité

I bug = dysfonctionnement logiciel

I problème : tous niveaux
I processeur, ex: bug virgule flottante des processeurs Pentium
I codage, ex : bug an 2000 (années codées sur deux chiffres),
2038 (langage C codé sur 32 bits)
I logiciel, ex : crash Ariane
I faille sécurité, ex : CB

Source: wikipedia, ...

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Chiffres et besoins

Bugs et qualité
I bug = dysfonctionnement logiciel
I problème : tous niveaux
I processeur, ex: bug virgule flottante des processeurs Pentium
I codage, ex : bug an 2000 (années codées sur deux chiffres),
2038 (langage C codé sur 32 bits)
I logiciel, ex : crash Ariane
I faille sécurité, ex : CB
I Un bug peut être :
I soit un non-respect de la spécification du système (c’est-à-dire
de la définition de ce que le système est censé faire),
I soit un comportement inattendu non couvert par la
spécification (par exemple, cas non prévu de deux actions
contradictoires à traiter simultanément, cas du bug de l’an
2000).

Source: wikipedia, ...

Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Chiffres et besoins

Bugs et qualité
I bug = dysfonctionnement logiciel
I problème : tous niveaux
I processeur, ex: bug virgule flottante des processeurs Pentium
I codage, ex : bug an 2000 (années codées sur deux chiffres),
2038 (langage C codé sur 32 bits)
I logiciel, ex : crash Ariane
I faille sécurité, ex : CB
I Solutions
I Les règles de programmation.
I Les techniques de programmation.
I Les méthodologies de développement.
I Le support des langages de programmation.
I Le test.
I Les méthodes formelles.

Source: wikipedia, ...

Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Chiffres et besoins

Bugs et qualité
I bug = dysfonctionnement logiciel
I problème : tous niveaux
I processeur, ex: bug virgule flottante des processeurs Pentium
I codage, ex : bug an 2000 (années codées sur deux chiffres),
2038 (langage C codé sur 32 bits)
I logiciel, ex : crash Ariane
I faille sécurité, ex : CB
I Solutions
I Méthodes formelles sont une solution parmi d’autres :
notation/modèle formel + sémantique bien définie + outillage

I indispensable pour les systèmes critiques, la certification, ...

Source: wikipedia, ...

Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Chiffres et besoins

Quelques domaines clés

Dans certains domaines d’activité, les spécifications formelles ont
acquis un droit de cité incontestable :
I les réseaux de PETRI sont largement utilisés pour spécifier et valider des
protocoles de communication, les logiques temporelles en sont une
alternative moins répandue.
I les grammaires formelles sont utilisées pour définir et analyser les
langages, notamment en théorie des langages de programmation.
I les automates à états finis permettent la modélisation de mécanismes
critiques dont la validation formelle est estimée nécessaire (moniteurs
temps réel, postes de commande).
I la logique formelle et les algèbres permettent de formaliser et de
démontrer des algorithmes essentiels.
I la théorie des ensembles est un support important des bases de données
relationnelles et des spécifications abstraites de systèmes.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Chiffres et besoins

Pour quoi utiliser ?

I Analyse et spécification :
I Description formelle des concepts clés du problème (domaine
d’application)
I Spécification formelle de la solution (comportement du système)
I Prototypage

I Conception architecturale et détaillée :

I Spécification formelle de l’interface des modules.
I Méthode rigoureuse de raffinement

I Codification :
I Preuves de programmes
I Synthèse automatique du code
I Utilisation d’assertions

I Tests
I Génération automatique des tests

Source: G. Tremblay
Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Bénéfices

I ”Devoir en arriver à une meilleure compréhension de l’élément à spécifier

en forçant l’analyste à être abstrait tout enétant précis à propos des
propriétés du système peut être plus gratifiant que d’avoir le document de
spécification lui-même.” [Win90].
I Impact positif de l’effort de formalisation.
I Spécifications explicites, précises, non-ambiguës.
I Base pour la mise en oeuvre et pour des vérifications formelles.
I Outils (manipulation, analyse, simulation, génération de tests).
I Base pour le développement des tests.

Source: G. Tremblay

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Applications
(quelques) succès et industriels concernés :
I Orly Val, Métro ligne 14 [méthode B]
I U. Oxford et IBM CICS [Z] / qualité + réduction des coût 9%
I NASA, Airbus, IBM, Microsoft, FT R&D, ...
Exemples ayant utilisé des méthodes classiques :
I Réingénierie du système CICS (IBM).
I Composants matériels (Inmos).
I Appareilsélectroniques (Tektronik).
I Outils pour l’analyse structurée.
I Contrôle du métro (Paris).
I Contrôle de trains (SNCF).
I Contrôle du trafic aérien (UK et USA).
I Contrôle de réacteurs nucléaires (Ontario, USA).
I Navette spatiale de la NASA (contrôleur de vol, GPS).
I Contrôle pour machine de radiothérapie.

Source: G. Tremblay, P. Poizat

Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Application 2/2
Exemples ayant utilisé la vérification de modèles :
I

I Protocole de cohérence de cache IEEE Futurebus+

(identification d’erreurs non détectées auparavant)
I Protocole de télécommunication ISDN/ISUP (122 erreurs
détectées)
I Contrôleur de canal HDLC (erreur majeure détectée)
I Système actif de contrôle des structures en génie civil (erreur
majeure détectée, qui aurait pû amplifier l’effet des vibrations)
I ...

Source: G. Tremblay

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Intérêts

I aux aspects formels :

I Des propriétés peuvent être établies par raisonnement formel, ce qui
n’est pas le cas des autres formes de spécification. Les preuves ne
sont plus intuitives mais basées sur une argumentation stricte.
I Les conséquences d’une spécification peuvent être mises en
évidence. Ainsi, les contradictions sont détectées avant la
réalisation.
I Les outils de preuve calculent et vérifient automatiquement et
uniquement ce qui a été décrit.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Intérêts

I aux aspects formels :

I à la précision :
I Le domaine du problème est mieux perçu. A force de réfléchir sur le
sujet, on le comprend mieux, les imprécisions sont levées, les
contradictions sont mises en valeur. Le problème est mieux compris.
I Le même langage est pratiqué par différentes personnes.
I Une conversion en langage naturel facilitera la discussion avec le
client, qui lui-même appréhende mieux le problème. On gagne en
clarté dans le dialogue.
I La spécification formelle est un avant-projet de la réalisation. Le
programmeur sait exactement ce qu’il doit programmer.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Intérêts
I aux aspects formels :
I à la précision :
I à l’abstraction (”quoi pas comment”),
I Une abstraction permet de ne retenir que les caractéristiques
essentielles,
I Une description abstraite est plus évolutive et perméable aux
changements des besoins, elle améliore la maintenabilité du logiciel
son accès.
I L’abstraction permet une distinction plus nette entre étude et
réalisation, pour lesquelles les choix et les décisions sont différents.
Une approche multi-language facilite la distinction.
I Les méthodes formelles mènent à des composants plus faciles à
réutiliser et plus fiables. On se rapproche en ce sens des techniques
d’autres “génies” (civil, mécanique, électrique).

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Inconvénients

I difficulté : les praticiens n’ont pas toujours la connaissance nécessaire.

Les formalismes ne sont pas toujours très lisibles ou accessibles. “Malgré
les progrès significatifs accomplis ces dernières années pour rendre les
notations formelles plus compréhensibles et utilisables, la rédaction et
l’emploi de spécifications formelles exigent toujours un certain niveau
d’aptitude mathématique, ainsi qu’un effort important.” [Mey92].
I diversité : plusieurs standards existent (Z, VDM, modèles algébriques,
OSDL, etc.).

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Inconvénients

I difficulté :
I diversité :
I pauvreté des processus et des outils support : peu de méthodes
présentent un processus clair et réaliste, un environnement complet et
convivial fait défaut même si des prototypes existent. Les preuves sont
souvent données de façon anecdotique dans les ouvrages. Le formalisme
doit permettre autant que possible d’automatiser la preuve.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Inconvénients

I difficulté :
I diversité :
I pauvreté des processus et des outils support :
I difficultés de modélisation : manque de structuration, erreurs,
exceptions, concurrence. On a besoin d’outils et de méthodes pour
construire les spécifications complexes. La modélisation passe aussi par la
capitalisation du savoir (modèles, méthodes utilisées).

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Inconvénients

I difficulté :
I diversité :
I pauvreté des processus et des outils support :
I difficultés de modélisation :
I adéquation : la spécification formelle aide à cerner les oublis et les
contradictions, mais on ne peut prouver que ce qui a été spécifié, pas ce
qui était (implicitement) souhaité par le client.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Inconvénients

I difficulté :
I diversité :
I pauvreté des processus et des outils support :
I difficultés de modélisation :
I adéquation :
I preuve : des outils de preuve existent (calcul de schémas en Z,
réécriture dans les algèbres), mais ils sont insuffisants. Des études sont en
cours pour les enrichir et donner les algorithmes de test et de preuve.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Inconvénients
I difficulté :
I diversité :
I pauvreté des processus et des outils support :
I difficultés de modélisation :
I adéquation :
I preuve :
I domaine d’application : actuellement, les spécifications formelles ne
sont appliquées qu’à un nombre réduit d’applications : “Nous avons
présenté dans ce texte une certaine manière d’aborder une petite classe de
problèmes informatiques, ...” [Abr84]. “Certains éléments des langages
de programmation (le parallélisme, l’arithmétique en virgule flottante, les
structures de données complexes) sont encore difficiles à modéliser de
manière satisfaisante.” [Mey92]. Le lecteur trouvera dans [BH96] un
certain nombre d’application “réaliste” de méthodes formelles.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Inconvénients
I difficulté :
I diversité :
I pauvreté des processus et des outils support :
I difficultés de modélisation :
I adéquation :
I preuve :
I domaine d’application :
I raffinage : la théorie du raffinage ou réification est relativement simple
à comprendre : on transforme petit à petit les structures de données et de
contrôle jusqu’à atteindre les langages de programmation. Il faut noter
que le nombre d’étapes de raffinage peut être important et que la preuve
du bien-fondé de la transformation est souvent très lourde. “Une relation
bien fondée ne contient pas de cycle” [Jon93].

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Applications et limites

Inconvénients
I difficulté :
I diversité :
I pauvreté des processus et des outils support :
I difficultés de modélisation :
I adéquation :
I preuve :
I domaine d’application :
I raffinage :
I structuration : on a besoin d’outils de structuration des spécifications
pour en simplifier l’écriture, l’accès la preuve et la réutilisation. Certains
outils existent (dérivation de shéma en Z, sous-typage et relation
d’importation dans les spécifications algébriques) mais ne sont pas
toujours suffisants.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Plan
Introduction

Motivations

Un exemple introductif

Les systèmes formels

La spécification formelle

Une classification des méthodes formelles

Exemples

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Exemple introductif

1. Description informelle
2. Modélisation avec Merise
I MCD
I MCT
I Critique
3. Modélisation avec Z
I Données
I Traitements
I Critique
4. Bilan

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Description informelle
L’administration veut gérer automatiquement les salles d’attente à
l’hôpital. Chaque salle a une capacité d’accueil limitée. Elles
portent un nom et sont situées à un emplacement précis de
l’hôpital. Les patients sont admis normalement ou en urgence. Les
patients admis en urgence sont appelés prioritairement vis-à-vis des
patients en admission normale. L’ordre d’appel est l’ordre d’arrivée,
compte-tenu des éventuelles urgences. Un patient appelé est reçu
et soigné par le docteur. Les soins ne sont pas interrompus par
l’arrivée d’un patient en urgence. On considère trois cas :
1. une seule salle d’attente et pas d’urgences,
2. une seule salle d’attente et traitement des urgences,
3. plusieurs salles d’attente et traitement des urgences.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Modélisation avec Merise (MCD)

attente normale
num_ordre_na
Patient SalleAttente
0,1
no_SecSoc_p 0,n no_s
nom_p X T nom_s
prénom_p 0,n localisation_s
adresse_p 0,1 nb_places_s
urgence
num_ordre_u

+ dictionnaire des données + explications

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Modélisation avec Merise (MCT)

Arrivée d'un
patient

Orientation des patients

Vérification du patient
Création éventuelle du patient
Evaluation des soins
Orientation du patient

Normale Urgence Refus

Admission
Patient
Admission Admission refusée
créé
normale urgente
(a) (b)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Modélisation avec Merise (MCT)

Admission Admission
normale urgente
(a) (b)

b prioritaire sur a
Soin
soins prodigués au patient

Patient
guéri
+ explications

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...
- Manque de précision

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...
- Manque de précision
I règles de gestion

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...
- Manque de précision
I règles de gestion
I contraintes entre associations

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...
- Manque de précision
I règles de gestion
I contraintes entre associations
I contraintes informelles

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...
- Manque de précision
I règles de gestion
I contraintes entre associations
I contraintes informelles
- Manque de sémantique formelle

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...
- Manque de précision
I règles de gestion
I contraintes entre associations
I contraintes informelles
- Manque de sémantique formelle
I Comment vérifier ?

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...
- Manque de précision
I règles de gestion
I contraintes entre associations
I contraintes informelles
- Manque de sémantique formelle
I Comment vérifier ?
I Comment prouver la correction ?

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCD)
+ Plus concis et moins soumis à interprétation que la description
informelle.
+ MCD presque complet (cardinalités, contraintes).
Mais ...
- Manque de précision
I règles de gestion
I contraintes entre associations
I contraintes informelles
- Manque de sémantique formelle
I Comment vérifier ?
I Comment prouver la correction ?
I Pas d’oublis ?

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...
- Manque de précision

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...
- Manque de précision
I règles de gestion

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...
- Manque de précision
I règles de gestion
I détails des opérations

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...
- Manque de précision
I règles de gestion
I détails des opérations
I contraintes sur les événements

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...
- Manque de précision
I règles de gestion
I détails des opérations
I contraintes sur les événements
- Manque de sémantique formelle

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...
- Manque de précision
I règles de gestion
I détails des opérations
I contraintes sur les événements
- Manque de sémantique formelle
I Comment vérifier ?

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...
- Manque de précision
I règles de gestion
I détails des opérations
I contraintes sur les événements
- Manque de sémantique formelle
I Comment vérifier ?
I Comment prouver la correction ?

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Critique (MCT)

+ Enchaı̂nements des opérations.

+ Vue globale des traitements.
Mais ...
- Manque de précision
I règles de gestion
I détails des opérations
I contraintes sur les événements
- Manque de sémantique formelle
I Comment vérifier ?
I Comment prouver la correction ?
I Pas d’oublis ?

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Merise

Exemple introductif

1. Description informelle
2. Modélisation avec Merise
I MCD
I MCT
I Critique
3. Modélisation avec Z
I Données
I Traitements
I Critique
4. Bilan

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Données)

Définitions de types, déclarations globales

[PATIENT ]
MAX =
b 20

Définitions de l’état du système (schéma)

SalleAttenteH ôpital
patients : seq PATIENT
#patients ≤ MAX
∀i, j : 1 . . #patients | i 6= j • patients(i) 6= patients(j)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Traitements)

Définitions des opérations de modification (schéma)
Arriv ée
∆SalleAttenteH ôpital
p? : PATIENT
patients 0 = patients _ hp?i
#patients < MAX ∧ ∀i : 1 . . #patients • patients(i) 6= p?

Sortie
∆SalleAttenteH ôpital
p! : PATIENT
patients = hp!i _ patients 0
patients 6= hi
Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Traitements)

Définitions des préconditions des opérations (schéma)

pre Arriv é =
b
∃SalleAttenteH ôpital 0 • Arriv ée

pre Arriv ée

SalleAttenteH ôpital
p? : PATIENT
#patients < MAX ∧
(∀i : 1 . . #patients • patients(i) 6= p?)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Traitements)

Définitions des opérations de consultation (schéma)

EnAttente
ΞSalleAttenteH ôpital
n! :IN
n! = #patients

Combien de patients en attente ?

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Traitements)

nième patient à consulter

Sorties
∆SalleAttenteH ôpital
p! : PATIENT
n? :IN 1
n? ≤ #patients
∃sa1 : seq PATIENT | #sa1 = n? − 1 •
patients = sa1 _ hp!i _ patients 0

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

Prouver des
I propriétés générales e.g.cohérence et complétude, équité, la
vivacité . . .

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

Prouver des
I propriétés générales e.g.cohérence et complétude, équité, la
vivacité . . .
I propriétés attendues du système.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

Prouver des
I propriétés générales e.g.cohérence et complétude, équité, la
vivacité . . .
I propriétés attendues du système.
I propriétés liées à la pratique de Z (ou VDM) (obligations de
preuves)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

Prouver des
I propriétés générales e.g.cohérence et complétude, équité, la
vivacité . . .
I propriétés attendues du système.
I propriétés liées à la pratique de Z (ou VDM) (obligations de
preuves)
I Existence d’un état initial.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

Prouver des
I propriétés générales e.g.cohérence et complétude, équité, la
vivacité . . .
I propriétés attendues du système.
I propriétés liées à la pratique de Z (ou VDM) (obligations de
preuves)
I Existence d’un état initial.
I Préservation des invariants dans les opérations.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

Prouver des
I propriétés générales e.g.cohérence et complétude, équité, la
vivacité . . .
I propriétés attendues du système.
I propriétés liées à la pratique de Z (ou VDM) (obligations de
preuves)
I Existence d’un état initial.
I Préservation des invariants dans les opérations.
I Preuve de raffinement de données ou d’opérations.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

I Les propriétés attendues pour le système salle d’attente sont :

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

I Les propriétés attendues pour le système salle d’attente sont :

I La capacité de la salle n’est pas dépassée.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

I Les propriétés attendues pour le système salle d’attente sont :

I La capacité de la salle n’est pas dépassée.
I Il y a équité (forte).

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

I Les propriétés attendues pour le système salle d’attente sont :

I La capacité de la salle n’est pas dépassée.
I Il y a équité (forte).
I L’ordre de sortie est l’ordre d’arrivée.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

I Les propriétés attendues pour le système salle d’attente sont :

I La capacité de la salle n’est pas dépassée.
I Il y a équité (forte).
I L’ordre de sortie est l’ordre d’arrivée.
I Conservation du nombre pour (arrivée + sortie . . . )

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

I Les propriétés attendues pour le système salle d’attente sont :

I La capacité de la salle n’est pas dépassée.
I Il y a équité (forte).
I L’ordre de sortie est l’ordre d’arrivée.
I Conservation du nombre pour (arrivée + sortie . . . )
I Les obligations de preuves sont :

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

I Les propriétés attendues pour le système salle d’attente sont :

I La capacité de la salle n’est pas dépassée.
I Il y a équité (forte).
I L’ordre de sortie est l’ordre d’arrivée.
I Conservation du nombre pour (arrivée + sortie . . . )
I Les obligations de preuves sont :
I Existence d’un état initial.
∃SalleAttenteH ôpital • InitSalleAttenteH ôpital ;

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Validation)

I Les propriétés attendues pour le système salle d’attente sont :

I La capacité de la salle n’est pas dépassée.
I Il y a équité (forte).
I L’ordre de sortie est l’ordre d’arrivée.
I Conservation du nombre pour (arrivée + sortie . . . )
I Les obligations de preuves sont :
I Existence d’un état initial.
∃SalleAttenteH ôpital • InitSalleAttenteH ôpital ;
I Préservation de l’invariant dans les opérations.
∃SalleAttenteH ôpital 0 ; sorties! • SchémaOp.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Raffinement)

De la spécification au code...
Deux types de raffinement sont distingués en Z :
I Le raffinement des opérations. Les structures de contrôle du
langage de programmation cible sont introduites
progressivement e.g.séquence, conditionnelles, itérations pour
la programmation impérative.
I Le raffinement des données. Les structures de données du
langage de programmation cible sont introduites
progressivement e.g.structures, tableaux, pointeurs pour la
programmation impérative.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Raffinement *)

[PATIENT ]
MAX = b 20

SalleConcret
file : seq PATIENT
premier :IN
#file ≤ MAX ∧ premier ≤ MAX
∀i, j : 1 . . premier | i 6= j • file(i) 6= file(j)

InitSalleConcret
SalleConcret
premier = 0

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Raffinement **)

Arriv éeC
∆SalleConcret
p? : PATIENT
premier < MAX ∧ ∀i : 1 . . premier • file(i) 6= p? ∧
premier 0 = premier + 1 ∧ file 0 = hp?i _ front file

pre Arriv éeC

SalleConcret
p? : PATIENT
premier < MAX ∧ ∀i : 1 . . premier • file(i) 6= p?

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Raffinement ***)

SortieC
∆SalleConcret
p! : PATIENT
premier > 0
premier 0 = premier − 1

pre SortieC
SalleConcret
p! : PATIENT
premier > 0

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Raffinement ****)

EnAttenteC
ΞSalleConcret
n! :IN
n! = premier

SortiesC
∆SalleConcret
p! : PATIENT
n? :IN 1
n? ≤ premier ∧ p! = file(n?) ∧
premier 0 = premier − n? ∧ file 0 = file

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Modélisation avec Z (Raffinement *****)

Abs
SalleAttenteH ôpital
SalleConcret
patients = rev ((1 . . premier ) / file)

Preuves du raffinement
I de l’état initial
I des opérations

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Exemple introductif

1. Description informelle
2. Modélisation avec Merise
I MCD
I MCT
I Critique
3. Modélisation avec Z
I Données
I Traitements
I Critique
4. Bilan

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)
+ Rigueur (types, contraintes, invariants, traitements)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)
+ Rigueur (types, contraintes, invariants, traitements)
+ Abstraction (vis à vis des langages de programmation)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)
+ Rigueur (types, contraintes, invariants, traitements)
+ Abstraction (vis à vis des langages de programmation)
⇒ Réduction des erreurs tardives, réutilisabilité en confiance

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)
+ Rigueur (types, contraintes, invariants, traitements)
+ Abstraction (vis à vis des langages de programmation)
⇒ Réduction des erreurs tardives, réutilisabilité en confiance

- pratique délicate (lisibilité, expérience)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)
+ Rigueur (types, contraintes, invariants, traitements)
+ Abstraction (vis à vis des langages de programmation)
⇒ Réduction des erreurs tardives, réutilisabilité en confiance

- pratique délicate (lisibilité, expérience)

- lourdeur de modélisation

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)
+ Rigueur (types, contraintes, invariants, traitements)
+ Abstraction (vis à vis des langages de programmation)
⇒ Réduction des erreurs tardives, réutilisabilité en confiance

- pratique délicate (lisibilité, expérience)

- lourdeur de modélisation
- temps de spécification et preuve

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)
+ Rigueur (types, contraintes, invariants, traitements)
+ Abstraction (vis à vis des langages de programmation)
⇒ Réduction des erreurs tardives, réutilisabilité en confiance

- pratique délicate (lisibilité, expérience)

- lourdeur de modélisation
- temps de spécification et preuve
- domaine d’application

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Bilan
Les ”spec formelles”
+ Formalisme (théories, logiques et calculs)
+ Rigueur (types, contraintes, invariants, traitements)
+ Abstraction (vis à vis des langages de programmation)
⇒ Réduction des erreurs tardives, réutilisabilité en confiance

- pratique délicate (lisibilité, expérience)

- lourdeur de modélisation
- temps de spécification et preuve
- domaine d’application
⇒ Application limitée

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Usage

Usage des ”spec formelles”

I réfléchir sur des spécifications avant d’implanter =
raisonnement abstrait

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Usage

Usage des ”spec formelles”

I réfléchir sur des spécifications avant d’implanter =
raisonnement abstrait
I prouver des propriétés avant de tester

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Usage

Usage des ”spec formelles”

I réfléchir sur des spécifications avant d’implanter =
raisonnement abstrait
I prouver des propriétés avant de tester
I prouver la correction de programmes

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Usage

Usage des ”spec formelles”

I réfléchir sur des spécifications avant d’implanter =
raisonnement abstrait
I prouver des propriétés avant de tester
I prouver la correction de programmes
I automatiser la construction de programmes

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Usage

Usage des ”spec formelles”

I réfléchir sur des spécifications avant d’implanter =
raisonnement abstrait
I prouver des propriétés avant de tester
I prouver la correction de programmes
I automatiser la construction de programmes
I se dégager des contraintes d’implantation

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Usage

Usage des ”spec formelles”

I réfléchir sur des spécifications avant d’implanter =
raisonnement abstrait
I prouver des propriétés avant de tester
I prouver la correction de programmes
I automatiser la construction de programmes
I se dégager des contraintes d’implantation
I documenter la réutilisation

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Modélisation avec Z

Pour aller plus loin

I Les systèmes formels, définitions, utilisation des spécifications
formelles, Intérêts et limites, Classification
=⇒ [AV01b] Chapitre 1
I What is this Theory Good for?
www.cs.auc.dk/∼luca/SV/use.html

I Palshikar, Girish Keshav (2001) Applying Formal

Specifications to Real-World Software Development, IEEE
Software, Novembre/Décembre, pp. 89-97
www.seg.etsmtl.ca/sylvie/LOG310/Textes/Palshikar.pdf

I van Lamsweerde, Axel (2000) Formal Specification: a

Roadmap, ACM Future of Software Engineering Conference,
Limerick, Irelande, pp. 149-159.
www.seg.etsmtl.ca/sylvie/LOG310/Textes/p147-lamsweerde.pdf

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Plan
Introduction

Motivations

Un exemple introductif

Les systèmes formels

La spécification formelle

Une classification des méthodes formelles

Exemples

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Système formel =
I langage formel

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Système formel =
I langage formel
I alphabet
I syntaxe → META-LANGAGE

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Système formel =
I langage formel
I alphabet
I syntaxe → META-LANGAGE

mots, expressions, termes, éléments, formules

→ acceptés ou pas

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Système formel =
I langage formel
I système formel
I axiomes
I règles d’inférence
règles de déduction (→ méta-langage d’inférence))

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Système formel =
I langage formel
I système formel
I axiomes
I règles d’inférence
règles de déduction (→ méta-langage d’inférence))

construction des mots, expressions, termes, éléments, formules

→ acceptés

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Utilisation d’un système formel ⇒

I sémantique (langage naturel, dénotationnelle,
opérationnelle...)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Utilisation d’un système formel ⇒

I sémantique (langage naturel, dénotationnelle,
opérationnelle...)
I interprétation
→ associer un sens (une valeur) aux expressions

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Utilisation d’un système formel ⇒

I sémantique (langage naturel, dénotationnelle,
opérationnelle...)
I interprétation
I calcul
I preuve = suite d’inférence
I théorème = expression prouvée

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Les systèmes formels

Utilisation d’un système formel ⇒
I sémantique (langage naturel, dénotationnelle,
opérationnelle...)
I interprétation
I calcul
I propriétés
I cohérence ⇒ deux expressions 6= ont des valeurs différentes
en logique : on ne peut déduire vrai = faux
I complétude ⇒ pas de valeur non-atteignables par les
expressions
en logique : chaque valeur ’vrai’ est prouvée par un théorème

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Plan
Introduction

Motivations

Un exemple introductif

Les systèmes formels

La spécification formelle

Une classification des méthodes formelles

Exemples

Méthodes formelles MIAGE

Exemples

MIAGE

Spécification
informelle
Classification

Elaboration Elaboration
du MCD du MCT
Processus

Schéma E-A-P MCT

corrections
Les systèmes formels

Validation
Traduction croisée
en Z
Spécification
Spécification de
l'état du système
Un exemple introductif

La spécification formelle

Spécification
des opérations
en Z
vérification
preuves et
Implantation
raffinement Implantation
Motivations

Méthodes formelles
Application
Tests
(ex: Pascal,
Vérifications
Caml, SGBDR)
Introduction
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Plan
Introduction

Motivations

Un exemple introductif

Les systèmes formels

La spécification formelle

Une classification des méthodes formelles

Exemples

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Une classification des méthodes formelles

Il existe de nombreuses approches plus ou moins parcellaires avec

de nombreuses variantes.
Site de référence :
http://archive.comlab.ox.ac.uk/formal-methods.html
maintenant http://formalmethods.wikia.com/wiki/VL
une centaine de méthodes référencées !!!

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Une classification des méthodes formelles

Il existe de nombreuses approches plus ou moins parcellaires avec

de nombreuses variantes.
Site de référence :
http://archive.comlab.ox.ac.uk/formal-methods.html
maintenant http://formalmethods.wikia.com/wiki/VL
une centaine de méthodes référencées !!!
I difficile de classer les approches
→ subjectif

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Une classification des méthodes formelles

Critères possibles :
I type de raisonnement

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Une classification des méthodes formelles

Critères possibles :
I type de raisonnement :
I structure (par modèle, opérationnel) :
I modèle mathématique : Z, B, VDM, AMN, automates,
réseaux de Petri...
I modèle algorithmique : CLU
I théorie des types : Coq,
I algèbres de processus : CSP, CCS, π-calcul, ...
I files d’attentes : SDL, QNAP, ...
I propriétés (axiomatique) : réécriture, LP, spécifications
algébriques (LPG, ASL, CLEAR, OBJ, PLUSS, LARCH,
CASL), λ-calcul, logiques temporelles (TLA, LTL...), logiques
diverses...
Pour chaque cas, il existe des approches hybrides (LOTOS, COLD,
RSL...)
Méthodes formelles MIAGE
Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Une classification des méthodes formelles

Critères possibles :
I type de raisonnement
I aspect du système :
I statique : Z, B, VDM, AMN...
I dynamique : automates, réseaux de Petri, SDL, CSP, CCS,
TLA, π-calcul ...
I fonctionnel : spécifications algébriques, λ-calcul
Pour chaque cas, il existe des approches hybrides (LOTOS, COLD,
RSL...)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Une classification des méthodes formelles

Critères possibles :
I type de raisonnement
I aspect du système
I langage :
I général : Z, B, VDM, spécifications algébriques, CLU...
I dédié : automates, réseaux de Petri, TLA, SDL, CSP, CCS,
π-calcul, λ-calcul...
Pour chaque cas, il existe des approches hybrides (LOTOS, COLD,
RSL...)

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Une classification des méthodes formelles

Critères possibles :
I type de raisonnement
I aspect du système
I langage

En général, les approches s’accompagnent d’outils de preuve.

Les approches sont des méthodes si : méthode + outils de
développement.

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Plan
Introduction

Motivations

Un exemple introductif

Les systèmes formels

La spécification formelle

Une classification des méthodes formelles

Exemples

Méthodes formelles MIAGE

Introduction Motivations Un exemple introductif Les systèmes formels Processus Classification Exemples

Exemples

1. Z
2. Spécification algébrique
3. Spécification algorithmique
4. B
5. LOTOS
ex.intro.pdf

Méthodes formelles MIAGE