"Principle of
Beneficent Difficulty
Difficulties, explicitly characterized and diagnosed, are the medium in
which a method captures its central insights into a problem. A method without
limitations, whose development steps are never impossible to complete,
whose stages diagnose and recognise no difficulty, must be very bad indeed.
Just think about it. A method without limitations and difficulties is saying one
of two things to you. Either it’s saying that all problems are easily solved. You
know that’s not true. Or else it’s saying that some problems are difficult, but
the method is not going to help you to recognise or overcome the difficult bits
when you meet them. Take your choice. Either way it’s bad news. "
Michael Jackson. Software Requirements and Specifications: A Lexicon of Principles,
Practices and Prejudices. Addison-Wesley and ACM Press, 1996
Sunday, March 27, 2016
Z
Z
L'exemple classique (fourni par Mike Spivey dans La notation Z, Masson, traduit par Michel Lemoine, 1994)
Le carnet d'anniversaire
Nous utilisons, quand c'est possible, la notation ASCII de B.
NOM et DATE sont des types de base (les SETS de B)
Voici de qu'en Z, on appelle des schémas :
DELTA déclare : connu, connu', anniversaire, anniversaire'. Le prime exprime l'état après l'opération.
Attention !
Vous avez bien lu. Ci-dessus, nous avons écrit = et non :=. Un schéma est un prédicat. Le saut de ligne exprime une conjection.
Le schéma AjoutAnniversaire donne le prédicat qui doit être respecté par l'opération d'ajout.
connu = connu'
anniversaire' = anniversaire
Un schéma va permettre de spécifier un état initial, lequel, comme en B, sert à s'assurer que l'on peut bien avoir un état satisfaisant les contraintes.
RAPPORT est un type libre.
Utilisation du schéma calculus :
On va avoir une spécification robuste
etc.
Nous avons présenté des schémas fermés. Les déclarations sont locales à ces schémas.
Il existe des schémas ouverts (description axiomatique) qui introduisent une ou plusieurs variables globales et éventuellement spécifient une contraintes sur leurs valeurs.
Exemple :
La notation Z pour la description des ensembles en compréhension :
{...| ... ....}
On distingue trois parties {déclaration | contrainte . expression }
exemple :
On peut prendre un schéma comme type.
Un schéma est alors vu comme l'ensemble des états qui respectent le schéma. Une variable de type schéma est alors une variable qui peut prendre comme valeur un de ces états qui respectent le schéma indiqué comme type de la variable.
Généricité
Exemple
Bibliographie
En français, deux livres sur Z.
Une introduction avec
D. Lightfoot, Spécification formelle avec Z, Teknea, traduit par H. Habrias
J.M. Spivey, La notation Z, Masson, traduit par M. Lemoine
L'exemple classique (fourni par Mike Spivey dans La notation Z, Masson, traduit par Michel Lemoine, 1994)
Le carnet d'anniversaire
Nous utilisons, quand c'est possible, la notation ASCII de B.
[NOM, DATE]
NOM et DATE sont des types de base (les SETS de B)
Voici de qu'en Z, on appelle des schémas :
______CarnetDAnniversaire______________
connu : POW (NOM)
anniversaire : NOM +-> DATE
_________________
connu = dom (naissance)
_____________________________________
_____AjoutAnniversaire__________________
DELTACarnetDAnniversaire
nom? : NOM
date? : DATE
________________
nom? /: connu
anniversaire' = anniversaire \/ {nom? |-> date?}
_____________________________________
DELTA déclare : connu, connu', anniversaire, anniversaire'. Le prime exprime l'état après l'opération.
Attention !
Vous avez bien lu. Ci-dessus, nous avons écrit = et non :=. Un schéma est un prédicat. Le saut de ligne exprime une conjection.
Le schéma AjoutAnniversaire donne le prédicat qui doit être respecté par l'opération d'ajout.
______ChercherAnniversaire________________KHI déclare : connu, connu', anniversaire, anniversaire' et les contraintes :
KHICarnetDAnniversaire
nom? : NOM
date! : DATE
________________
nom? : connu
date! : anniversaire (nom?)
_______________________________________
connu = connu'
anniversaire' = anniversaire
Un schéma va permettre de spécifier un état initial, lequel, comme en B, sert à s'assurer que l'on peut bien avoir un état satisfaisant les contraintes.
______InitCarnetDAnniversaire________________
CarnetDAnniversaire
_____________________
connu = { }
________________________________________ RAPPORT ::= ok | déjàConnu | nonConnu
RAPPORT est un type libre.
____Succès______________________________
résultat! : RAPPORT
___________________
résultat! = ok
________________________________________
____DéjàConnu___________________________
KHICarnetDAnniversaire
nom? : NOM
résultat! : RAPPORT
_______________________
nom? : connu
résultat! = déjàConnu
________________________________________
Utilisation du schéma calculus :
On va avoir une spécification robuste
Il y a d'autres opérateurs que le & et le or pour le calcul de schémas.
RAjoutAnniversaire == (AjoutAnniversaire & Succès) or DéjàConnu
etc.
Nous avons présenté des schémas fermés. Les déclarations sont locales à ces schémas.
Il existe des schémas ouverts (description axiomatique) qui introduisent une ou plusieurs variables globales et éventuellement spécifient une contraintes sur leurs valeurs.
Exemple :
carré : NAT --> NAT
_________________
! b: NAT . carré(n) = n * n
La notation Z pour la description des ensembles en compréhension :
{...| ... ....}
On distingue trois parties {déclaration | contrainte . expression }
exemple :
{x : NAT | pair (x) . x * x} est l'ensemble des carrés des nombres pairs.Les schémas comme types
On peut prendre un schéma comme type.
Un schéma est alors vu comme l'ensemble des états qui respectent le schéma. Une variable de type schéma est alors une variable qui peut prendre comme valeur un de ces états qui respectent le schéma indiqué comme type de la variable.
Généricité
Exemple
=======[X, Y] =============================
first : X * Y --> X
___________________
!x : X ; y : Y . first(x, y) = x
_________________________________________
Bibliographie
En français, deux livres sur Z.
Une introduction avec
D. Lightfoot, Spécification formelle avec Z, Teknea, traduit par H. Habrias
J.M. Spivey, La notation Z, Masson, traduit par M. Lemoine
B événementiel, l'île et le pont de J.R. Abrial
Source : Présentation de J.R. Abrial (Janvier 2000)
Le contrôleur du pont de l'île
Le principe : le saut en parachute.
Quelles sont les données ?
On a une seule variable, n, le nombre de véhicules qui sont dans le système.
De plus, le nombre maximum de véhicules que peut contenir le système est constant (d)
La contrainte à satisfaire est :
On a deux événements
Sortie du continent vers le système
Entrée sur le continent
Les obligations de preuve
1) La préservation de l'invariant
Soit dans notre cas
pour l'événement ML_OUT
0 <= n <= d & n0 <= n + 1 <= d
pour l'événement ML-IN
0 <= n <= d & n0 <= n - 1 <= d
2) Preuve de vivacité (liveness)
Soit ici :
0 <= n <= d => 0 < n or n < d
Ce que l'on ne peut prouver !
Quand n = 0, on ne peut prouver n < d
On a oublié 0 < d
Il y a un deadlock si d = O (plus aucune voiture ne peut entrer).
On corrige donc et alors on peut prouver que :
0 <= n <= d & 0 < d => 0 < n or n < d
3) Preuve d'absence de sous-boucles infinies
Pour chaque événement (dans le cas de deux événements seulement) :
Soit ici
Pour ML_OUT, un variant est d - n
0 <= n <= d & 0 < d => 0 <= d - n
0 <= n <= d & 0 < d & n < d
=>
d - (n + 1) < d - n
Pour ML_IN, un variant est n
0 <= n <= d & 0 < d => 0 <= n
0 <= n <= d & 0 < d & n < d
=>
n -1 < n
Deuxième vue du système , raffinage par introduction du pont
On est descendu et on aperçoit maintenant le pont.
On voit :
Invariant de collage
Les techniques de raffinage :
Les mécanismes de raffinage sont :
Dans notre cas,
1) Raffinage de l'événement abstrait
ML_OUT == WHEN n < d THEN n := n + 1 END
en :
ML_OUT ==
WHEN
a + b + c < d & c = 0 /* On a renforcé la garde */
THEN
a := a + 1
END
Raffinage de l'autre événement abstrait :
ML_IN ==
WHEN
n > 0
THEN
n := n + 1
END
en :
ML_IN ==
WHEN
c > 0
THEN
c := c - 1
END
2) Spécification des nouveaux événements
IL_IN ==
WHEN
a > 0
THEN
a, b := a - 1, b + 1
END
IL_OUT ==
WHEN
b > 0 &
a = 0
THEN
b, c := b - c, c + 1
END
Les obligations de preuve du raffinage d'événement
...
à vous maintenant d'appliquer cela...
Les niveaux suivants seront :
1) Introduction de deux feux de circulation à chaque entrée du pont
2) Introduction de capteurs (il faut bien compter les véhicules pour vérifier l'invariant fourni au premier niveau) à l'entrée et à la sortie du pont
Puis introduction du contrôleur qui :
- qui représentent ce que le contrôleur croit de la situation physique
- dont les valeurs peuvent être différentes de celles des variables physiques
mais néanmoins le système doit fonctionner correctement comme celà est prescrit par les vairiables physiques
- conservées en mémoire du contrôleur
3) Introduction des canaux de communication
- entre le monde physique et le contrôleur (annonce de l'arrivée ou du départ d'un véhicule)
- entre le contrôleur et le monde physique (pour faire changer)
Des hypothèses temporelles doivent être faites (par exemple que les capteurs physiques sont moins réactifs que les autres événements)
4) Réunion des variables physiques et des variables canaux pour former une seule entité, l'environnement fait de :
- des variables physiques et des variables canaux
- tous les événements physiques
- deux services d'entrée/sortie
Le contrôleur du pont de l'île
Le principe : le saut en parachute.
Plus on s'approche du sol, plus on voit de choses, plus on voit d'événements.Première vue du système (ou modèle initial)
Quelles sont les données ?
On a une seule variable, n, le nombre de véhicules qui sont dans le système.
De plus, le nombre maximum de véhicules que peut contenir le système est constant (d)
La contrainte à satisfaire est :
0 <= n <= dLa forme générale d'un événement pour cette présentation
==
WHEN
< garde>
THEN
< action>
END
On a deux événements
Sortie du continent vers le système
ML_OUT ==
WHEN
n < d
THEN
n := n+ 1
END
Entrée sur le continent
ML_IN ==
WHEN
n > 0
THEN
n := n - 1
END
Les obligations de preuve
1) La préservation de l'invariant
Etant donné un événement de forme générale : EVENT ==
WHEN
G(x)
THEN
x := E(x)
END
et un invariant I(x) à préserver, il faut prouver que :
I(x) & G(x) => I(E(x))
Soit dans notre cas
pour l'événement ML_OUT
0 <= n <= d & n
pour l'événement ML-IN
0 <= n <= d & n
2) Preuve de vivacité (liveness)
Etant donné un système d'événements avec les gardes :
G1 (x), ..., Gn (x) et un invariant I(x), l'énoncé à prouver est :
I(x) => G1(x) or ...or Gn(x)
i.e. un événement au moins est toujours prêt à être déclenché (ABSENCE DE VERROU FATAL)
Soit ici :
0 <= n <= d => 0 < n or n < d
Ce que l'on ne peut prouver !
Quand n = 0, on ne peut prouver n < d
On a oublié 0 < d
Il y a un deadlock si d = O (plus aucune voiture ne peut entrer).
On corrige donc et alors on peut prouver que :
0 <= n <= d & 0 < d => 0 < n or n < d
3) Preuve d'absence de sous-boucles infinies
Pour chaque événement (dans le cas de deux événements seulement) :
EVENT ==
WHEN G(x) THEN x := E(x) END Il faut prouver, étant donné un invariant I(x) :
I(x) => 0 <= V(x) &
I(x) & G(x) =< V (E(x)) < V(x)
où V(x) est un variant à exhiber pour chaque événement.
Soit ici
Pour ML_OUT, un variant est d - n
0 <= n <= d & 0 < d => 0 <= d - n
0 <= n <= d & 0 < d & n < d
=>
d - (n + 1) < d - n
Pour ML_IN, un variant est n
0 <= n <= d & 0 < d => 0 <= n
0 <= n <= d & 0 < d & n < d
=>
n -1 < n
Deuxième vue du système , raffinage par introduction du pont
On est descendu et on aperçoit maintenant le pont.
On voit :
- des véhicules sur le pont qui se dirigent vers l'île (un nombre n)L'invariant
- des véhicules qui sont dans l'île (un nombre b)
- des véhicules qui se dirigent vers le contenant (un nombre c)
0 <= a &
0 <= b &
0 <= c &
a = 0 or c = 0 /* tous les véhicules vont dans la même direction */
Invariant de collage
a + b + c = n
Les techniques de raffinage :
1) Chaque événement est raffiné par un événement concret 2) Le monde abstrait travaille avec x et le concret avec y
3) Un invariant de collage I(x, y) lie les deux mondes
Les mécanismes de raffinage sont :
- le renforcement des gardes (normal, plus on voit de choses en s'approchant du sol, plus on voit de contraintes. C'est bien connu, quand on est "haut placé" on est en dehors des contingences matérielles...voilà sans doute pourquoi certains recherchent ces places...dans les amphis (?!)) Rappel : en ce qui concerne les préconditions, on les affaiblit lors du raffinage.
- des actions "simultanées" sur l'invariant de collage.
Dans notre cas,
1) Raffinage de l'événement abstrait
ML_OUT == WHEN n < d THEN n := n + 1 END
en :
ML_OUT ==
WHEN
a + b + c < d & c = 0 /* On a renforcé la garde */
THEN
a := a + 1
END
Raffinage de l'autre événement abstrait :
ML_IN ==
WHEN
n > 0
THEN
n := n + 1
END
en :
ML_IN ==
WHEN
c > 0
THEN
c := c - 1
END
2) Spécification des nouveaux événements
IL_IN ==
WHEN
a > 0
THEN
a, b := a - 1, b + 1
END
IL_OUT ==
WHEN
b > 0 &
a = 0
THEN
b, c := b - c, c + 1
END
Les obligations de preuve du raffinage d'événement
Etant donné un événement abstrait et un événement concret correspondant EVENT == WHEN G(x) THEN x := E(x) END
EVENT == WHEN H(y) THEN y := F(y) END
et les invariant I(x) (supposé être déjà préservé par l'événement abstrait) et J(x, y),
I(x) & J(x, y) & H(y) => G(x)
I(x) & J(x, y) & H(y) => J(E(x), F(y))
...
à vous maintenant d'appliquer cela...
Les niveaux suivants seront :
1) Introduction de deux feux de circulation à chaque entrée du pont
2) Introduction de capteurs (il faut bien compter les véhicules pour vérifier l'invariant fourni au premier niveau) à l'entrée et à la sortie du pont
Puis introduction du contrôleur qui :
- décide quand les feux doivent changer
- n'a pas accès aux variables physiques
- a accès à des variables de contrôle
- qui sont des copies de variables physiques
- qui représentent ce que le contrôleur croit de la situation physique
- dont les valeurs peuvent être différentes de celles des variables physiques
mais néanmoins le système doit fonctionner correctement comme celà est prescrit par les vairiables physiques
- conservées en mémoire du contrôleur
3) Introduction des canaux de communication
- entre le monde physique et le contrôleur (annonce de l'arrivée ou du départ d'un véhicule)
- entre le contrôleur et le monde physique (pour faire changer)
Des hypothèses temporelles doivent être faites (par exemple que les capteurs physiques sont moins réactifs que les autres événements)
4) Réunion des variables physiques et des variables canaux pour former une seule entité, l'environnement fait de :
- des variables physiques et des variables canaux
- tous les événements physiques
- deux services d'entrée/sortie
Z twenty years on, What is its future? (1995)
====================================================
Simple text version
====================================================
INSTITUT de RECHERCHE en INFORMATIQUE de NANTES (IRIN)
Universit'e de Nantes - Ecole Centrale de Nantes
with the assistance of
Institut Universitaire de Technologie (Dpt. Informatique) and
``Software Engineering Methods Group'' of IRIN and
with the participation of the B User Group
First Call for Communications
In the series of conferences :
``Putting into Practice, Methods and Tools for Information System Design''
Z twenty years on
What is its future?
10th - 11th - 12th October 1995
NANTES (France)
One may consider J.R. Abrial's publication ``Data Semantics'' in 1974,
as the birth of what was to become the formal notation Z. Z was developed
to its present stateat Oxford's Programming Research Group. J.R. Abrial continued
this work which led to the method B.
The general theme of this conference is ``Z and its future''
Nowadays we find different forms of Z. What are their advantages and
weaknesses?
A great deal has been written on Z but what of its use for full scale
development?
How can Z be introduced into industrial information system design?
What is the situation in comparison with semi-formal methods?
How can Z be introduced into an industrial way of thinking and industrial
practice?
Z is a notation for specification, but it is then necessary to produce program
code. What are the techniques which may be involved for the production of
programs, from Z specifications?
Proposals to present a paper, or demonstrate software, or present
a case-study, should be submitted to H. Habrias at the address below.
4 copies of the proposals must be received by 1st May 1995
(PostScript E-mail non-european contributions are accepted.)
Notification of acceptance 20 June 1995, final version due on 15 July.
Themes :
Methods for using Z,
Styles of specification,
Comparing different versions of Z, and Z and B,
Comparing Z, B and other formal methods,
State based methods and semi-formal methods,
Supporting software tools,
Specification implementation,
Specification animation,
Reactive systems,
Estimation of the adequacy of the specifications,
Specification and certification
Articles concerning applications to industrial cases and pedagogic cases will be appreciated.
The conference will consist of a day of lectures and a day of case-study presentations.
Languages : English and French.
The proceedings will be published.
Programme Committee : J.R. Abrial (Consultant, Paris, F),
D. Bert (IMAG, Grenoble), J.P. Bowen (representative of the ZUM conference,
Oxford University, G.B.), D. Buchs (E.P.F.L., Lausanne, CH), J.Y. Chauvet
(Caisse Nat. D'assurance Viellesse, Tours, F), C. Choppy (LRI, Un. Orsay, F),
D. Garlan (Carnegie Mellon University, USA), M. Gondran (EDF, Clamart, F),
I. Hayes (University of Queensland, Australia), G. Laffitte (INSEE, Nantes, F),
M. Lemoine (CERT-ONERA, Toulouse, F), D. Lightfoot (Oxford Brookes University,
UK),
F. Mejia (GEC-Alsthom, Paris, F), S.A. Schuman (Surrey University, G.B.), M.
Weber (Technische Universitat, Berlin).
Organisation Committee : Software Engineering Methods Group of IRIN
H. HABRIAS
IUT de Nantes
3 Rue du Marechal Joffre,
44041 NANTES Cedex 01 (France)
Tel : 33 40 30 60 52/60 53
Fax : 33 40 30 60 01/60 53
E-mail : Z2B@iut-nantes.univ-nantes.fr
The proceedings for the years : 87, 88, 89, 90, 91 are available.
Lectures by J.R. Abrial, ``Introduction to the Method B'' are available
on video cassettes lasting 6 hours, from Teknea, Toulouse.
Proceedings :
Formally Checking Large Data Sets in the Railways
http://arxiv.org/ftp/arxiv/papers/1210/1210.6815.pdf
This article presents industrial experience of validating large data sets against specification written using the B / Event-B mathematical language and the ProB model checker.
First B Conference, Program
FIRST B CONFERENCE
Nantes, November 25-26-27, 1996
PROGRAM
 | |
November 25, 1996 | |
- 08h 00
- Registration
- 08h 50
- Opening address by J.F. Nicaud, Directeur de l'IRIN
 | |
Session 1: Invited conference | |
- 09h 00
- L'échec du vol Ariane 501
Invited speaker : Gilles Kahn (Directeur scientifique, INRIA, Sophia-Antipolis) - 10h 00
- Break
| |
Session 2 | |
- 10h 30
- Développement formel des logiciels sécuritaires de METEOR
Patrick Behm (MATRA Transport International, Montrouge, F) - 11h 15
- Safety Critical Software Assessment: Past Experience and New Approach
Miloudi El Koursi, Georges Mariano (INRETS-ESTAS, Villeneuve d'Ascq, F) - 12h 00
- Break
| |
Session 3 | |
- 14h 00
- Experiences with Proof in a Formal Development
D. Clutterbuck, J. , B. Matthews
(Praxis Critical Systems, Bath, U.K.)
(Rutherford Appleton Lab., Oxon, U.K.) - 14h 45
- A Study on Components and Assembly Primitives in B
D. Bert, M.-L. Potet, Y. Rouzaud. (IMAG-LSR, Grenoble, F) - 15h 30
- Break
| |
Session 4 | |
- 16h 00
- La construction de la spécification formelle d'un système complexe
Nestor Lopez (groupe PI, CEDRIC, CNAM, Paris, F) - 17h 00
- Obligations de preuves de raffinement en B
Lilian Burdy (MATRA Transport Inter., Montrouge, F) - 17h 40
- Object-Oriented Modelling in B
Richard Shore (University of Teesside, Middlesbrough, UK) - 19h 00
- Soirée cabaret with the group ``Hélène et Jean-François''
 | |
November 26, 1996 | |
| |
Session 5 | |
- 09h 00
- Distributed System Developement in B
M. Butler (Univ. of Southampton, UK),
M. Walden (Abo Akademi University, Turku, Finland) - 09h 45
- Break - Formal specification books on exhibit
| |
Session 6 : Extending B | |
- 10h 15
- Extending B without Changing it (for Developing Distributed Systems)
Invited speaker: Jean-Raymond Abrial (Consultant independant, Paris, F) - 11h 00
- Machines Abstraites Temporelles. Analyse Comparative de B et de TLA+
Dominique Méry (Univ. de Nancy I, CRIN, Institut Univ. de France, F) - 11h 45
- Hypersubstitutions : Extending the Generalised Substitution to Model Semi-decidable Operations
Steve Dunne, Bill Stoddart (University of Teesside, Middlesbrough, UK) - 12h 30
- Break
| |
Session 7 : Experiences with B | |
- 14h 00
- Using B to Design and Verify Controllers for Chemical Processing
K. , J. Bicarregui, A. Sanchez
(Imperial College, London, U.K.) - 14h 45
- Dérivation de spécifications formelles B à partir de spécifications semi-formelles de systèmes d'information
P. Facon, R. Laleau, H.P. Nguyen (CEDRIC-IIE, CNAM, F) - 15h 30
- Break - Formal specification books on exhibit
| |
Session 8 | |
- 16h 00
- Early Experiences in Teaching the B-Method
Ken Robinson (University of New South Wales, Sydney, Australia) - 16h 40
- Proving on a Reasonable Level of Abstraction with Programmer-Designed Theories
Philip Heuberger (Turku Center of C.S., Turku, Finland) - 17h 00
- End
| |
November 27, 1996 | |
| |
Session 9 : Case Studies (A) | |
- 09h 00
- The Use of the B Method on an Avionics Example - The MIST ProjectInvited speaker: Jonathan Draper (GEC-Marconi Avionics Ltd,Rochester, UK)
- 09h 45
- Formal Development in B of a Minimum Spanning Tree Algorithm
Ranan Fraer (INRIA, Sophia-Antipolis, F) - 10h 30
- Break
| |
Session 10 : Case Studies (B) | |
- 11h 00
- Une étude de cas en B : les feux tricolores
Jean-Yves Chauvet (CNAM, Tours, F) - 11h 45
- Prizes
- for the best oral presentation
- for the best written paper
- 13h 00
- End of the conference
Subscribe to:
Posts (Atom)
