Sunday, March 27, 2016

Principle of Beneficent Difficulty, M. Jackson

 "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

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, 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________________
    KHICarnetDAnniversaire
    nom? : NOM
    date! : DATE
________________
    nom? : connu
    date! : anniversaire (nom?)
_______________________________________
  KHI déclare : connu, connu', anniversaire, anniversaire' et les contraintes : 
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 
 
RAjoutAnniversaire == (AjoutAnniversaire & Succès) or DéjàConnu
Il y a d'autres opérateurs que le & et le or pour le calcul de schémas. 
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. 


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 <= d
La 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 0 <= n + 1 <= d 
pour l'événement ML-IN 
0 <= n <= d & n 0 <= n - 1 <= d 
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)
- des véhicules qui sont dans l'île (un nombre b)
- des véhicules qui se dirigent vers le contenant (un nombre c)
L'invariant 
  
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 :

EAN13
9782906082199
ISBN
978-2-906082-19-9
Éditeur
IUT
Date de publication
Langue
anglais

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.
Comments:In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012
Subjects:Software Engineering (cs.SE)
Cite as:arXiv:1210.6815 [cs.SE]
 (or arXiv:1210.6815v2 [cs.SE] for this version)


See also :http://www.data-validation.fr/data-validation-in-the-railways/

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

Chairman, Pierre Desforges (RATP, Paris, F)
09h 00
L'échec du vol Ariane 501
Invited speaker : Gilles Kahn (Directeur scientifique, INRIA, Sophia-Antipolis)
10h 00
Break

Session 2

Chairman, J.L. Dormoy (EDF-DER, Clamart, F)
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

Chairman, Stephen Shirlaw (GEC Alsthom Signalling Ltd, London, UK)
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

Chairman, J.F. Monin (, Lannion, F)
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

Chairman, Thérèse Hardin (Univ. Paris VI, Paris)
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

Chairman, M. Frappier (Univ. de Sherbrooke, Canada)
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

Chairman, Steve Dunne (Un. of Teesside, UK)
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

Chairman, J.M. Meynadier (Matra Transport, F)

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)

Chairman, Didier Bert (LGI-IMAG, Grenoble)
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)

Chairman, Guy Laffitte (INSEE, Nantes, F)
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