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