ABZ 2018

5-8 June 2018, Southampton, U.K.

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

ABZ 2016

http://www.cdcc.faw.jku.at/ABZ2016/

ABZ 2016

ASM, Alloy, B, TLA, VDM, Z

May 23-27, 2016

Linz, Austria

Accepted Papers

http://www.cdcc.faw.jku.at/ABZ2016/accepted/

ABZ 2016

http://www.cdcc.faw.jku.at/ABZ2016/call4papers/

The ABZ conference is dedicated to the cross-fertilization of six related state-based and machine-based formal methods, Abstract State Machines (ASM), Alloy, B, TLA, VDM and Z, that share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. It builds on the success of the first ABZ conference held in London in 2008, where the ASM, B and Z conference series merged into a single event, the second ABZ 2010 conference held in Orford (Canada), where the Alloy community joined the event, the ABZ 2012 held in Pisa (Italy), which saw the inclusion of the VDM community, and ABZ 2014 held in Toulouse (France), which brought the inclusion of the TLA community into the ABZ conference series. The ABZ 2016 conference will be held in Linz, Austria.

Contributions are solicited on all aspects of the theory and applications of ASMs, Alloy, B, TLA, VDM, Z approaches in software/hardware engineering, including the development of tools and industrial applications. The program spans from theoretical and methodological foundations to practical applications, emphasizing system engineering methods and tools that are distinguished by mathematical rigor and have proved to be industrially viable. The main goal of the conference is to contribute to the integration of accurate state- and machine-based system development methods, clarifying their commonalities and differences to better understand how to combine different approaches for accomplishing the various tasks in modeling, experimental validation, mathematical verification of reliable high-quality hardware/software systems.

Although organized to host several formal methods with ASM, Alloy, B, TLA, VDM and Z, in a single event, editorial control of the joint conference is vested in one integrated program committee, which will respectively determine its ASM, Alloy, B, TLA, VDM and Z content, to be presented in parallel conference tracks with a schedule to allow the participants to switch between the sessions.

As successfully practiced at ABZ 2014, the 5th edition of ABZ will include again special sessions dedicated to a shared real-life case study among all the methods addressed in ABZ 2016. The objective of this session is to enrich the set of case studies developed with ABZ methods with a practical and real-life case study. After the success of the “Landing Gear” case study at ABZ 2014 in the aeronautical context this time the organizers defined a real-life case study issued from the medical domain with challenging safety requirements. The ABZ 2016 case study emphasizes the control of a hemodialysis machine. See http://www.cdcc.faw.jku.at/ ABZ2016/HD-CaseStudy.pdf for a detailed description of this case study.

Submission of Papers

Proposals are invited for workshops and tutorials to take place before the main conference.

Four kinds of contributions are invited:

• Research papers: full papers of not more than 14 pages in LNCS format, which have to be original, unpublished and not submitted elsewhere.
• Short presentations of work in progress, and tool demonstrations. This is an excellent opportunity for Ph.D. students to present and validate their work in progress. An extended abstract of not more than 4 pages is expected and will be reviewed.
• Answers to case study papers: full papers of not more than 14 pages in LNCS format reporting on the experiments conducted with any of the state based techniques in the scope of ABZ 2016.
• Application in industry papers reporting on work or experiences on the application of state based formal methods in industry. An extended abstract of not more than 4 pages is expected and will be reviewed. It is also an interesting option for industrial practitioners who sometimes face too many constraints to prepare a full paper.

Contributions should be submitted electronically in PDF at the ABZ 2016 conference submission website (Easy Chair).

The papers must be prepared using the SPRINGER LNCS style. The answers to case study should be submitted electronically in PDF at the ABZ 2016 case study submission website (Easy Chair)".

All research and short accepted papers will be published in a volume of Springer's LNCS series. The answers to case study papers and the application in industry papers will be published in a volume of Springer's CCIS series. The two volumes will be distributed at the conference.

Journal Special Issues

It is planned that an improved version of a selected number of contributions will be published in a special issue of the journal Science of Computer Programming for the research papers and in a special issue of the Software Tools and Technology Transfer journal for the answers to case study papers (to be confirmed).

Workshop Proposals

Workshops and tutorials will be associated to the main event ABZ. Proposals are solicited in areas related to the conference topics. Workshop proposal should be sent to the workshop chairs.

The deadline for submissions is October 16, 2015. Notifications will be sent by November 6, 2015.

Tutorial Proposals

Tutorial proposal should be sent to the tutorial chairs.

The deadline for submissions is February 15, 2016. Notifications will be sent by March 14, 2016.

Important Dates

Research paper and answers to case study submission:	January 15, 2016
Short paper submission:	February 04, 2016
Workshop proposal submissions:	October 16, 2015
Workshop proposal notifications:	November 06, 2015
Tutorial proposal submissions:	February 15, 2016
Acceptance notification:	February 22, 2016
Tutorial proposal notifications:	March 14, 2016
Final Version due:	March 14, 2016
Main ABZ 2016 conference:	May 23-27, 2016

Program Committee Chairs

• Michael BUTLER, University of Southampton, Southampton, UK
• Klaus-Dieter SCHEWE, Johannes-Kepler-Universität Linz and Software Competence Center Hagenberg, Linz/Hagenberg, Austria

Case Study Chairs

• Atif Mashkoor, Software Competence Center Hagenberg, Hagenberg, Austria (atif.mashkoor@scch.at)
• Miklos Biro, Software Competence Center Hagenberg, Hagenberg, Austria (miklos.biro@scch.at)

Tutorial Chairs

• Vincenzo Gervasi, Università di Pisa, Pisa, Italy (gervasi@di.unipi.it)
• Michael Leuschel, Universität Düsseldorf, Düsseldorf, Germany (leuschel@cs.uni-duesseldorf.de)

Workshop Chairs

• Yamine Ait-Ameur, Institut National Polytechnique de Toulouse, France (yamine@enseeiht.fr)
• Stephan Merz, INRIA Nancy, Nancy, France (stephan.merz@loria.fr)
• Alexander Raschke, Universität Ulm, Ulm, Germany (alexander.raschke@uni-ulm.de)

Program Committee

Program committee will be announced at a later date.

Conference Organizers

• Klaus-Dieter SCHEWE, Johannes-Kepler-Universität Linz and Software Competence Center Hagenberg, Linz/Hagenberg, Austria (Klaus-Dieter.Schewe@scch.at)
• Atif Mashkoor, Software Competence Center Hagenberg, Hagenberg, Austria (atif.mashkoor@scch.at)
• Mariam Rady, Johannes-Kepler-Universität Linz (m.rady@cdcc.faw.jku.at)
• Mircea Boris VLEJU (webmaster), Johannes-Kepler-Universität Linz (b.vleju@cdcc.faw.jku.at)
• Martina Höller, Software Competence Center Hagenberg, Hagenberg, Austria (martina.hoeller@scch.at)

For questions concerning ABZ 2016, contact Klaus-Dieter SCHEWE (Klaus-Dieter.Schewe@scch.at).

APCB, Association de Pilotage des Conférences Internationales B (International B Conferences Steering Comittee)

Le nouveau bureau de l'association élu par l'AG de Toulouse le 6 juin 2014 est composé de :

Dominique Méry, Président, professeur des universités, Université de Nancy (France)

Jean-Raymond Abrial, Vice-Président, consultant,Marseille (France)

Jérémie Christian Attiogbé, secrétaire, professeur des universités, Université de Nantes (France)

Henri Habrias, trésorier, professeur des universités retraité, Université de Nantes (France)

Yamine Ait Ameur, documentaliste,  professeur des universités, Toulouse (France)

Michael Butler, Professor of Computer Sciences, University of Southampton (U.K.)

Papers of the ABZ 2014 Conference

http://www.informatik.uni-trier.de/~ley/db/conf/asm/abz2014.html

ABZ Conference, Toulouse, quelques photos

The B International Conferences

*Conference Z2B, Nantes, France,oct. 10-12 1995
*First B Conference, Nantes, France,nov. 25-27 1996
*Second B Conference,Montpellier, France, ap. 22-24 1998,
*ZB'2000, York, U.K. 28 aug, 2 sept. 2000,
*ZB'2002, Grenoble, France, 23-25 jan. 2002,
*ZB'2003, Turku, Finlande, 4-6 jun. 2003
*ZB'05, Guildford, U.K., 2005
*B'2007, Besançon, France, 2007
*B, from research to teaching, Nantes,France, 16 juin 2008
*B, from research to teaching, Nantes,France, 8 juin 2009
*B, from research to teaching, Nantes,France, 7 juin 2010
*ABZ conference: ABZ 2008, British Computer Society, London, UK, 16-18 September 2008
*ABZ conference: ABZ 2010,Oxford, Québec, Canada, 23–25 February 2010
*ABZ conference: ABZ  2012, Pisa, Italy, 18-22 June 2012
*ABZ coference: ABZ 2014, Toulouse, France, 2-6 June 2014

The first "B International Conferences"

http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/ConfZetBdeNantes/ConfZBNantes.html

4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z June 2 - 6 2014 Toulouse - France

http://www.irit.fr/ABZ2014/index.html

Important dates

Research paper and answers to case study submission:	January 14, 2014
Workshop proposal submissions:	October 15, 2013
Short paper submission:	February 3, 2014
Tutorial proposal submissions:	January 30, 2014
Papers/abstract/answers to case study notification:	March 1, 2014
Workshop proposal notifications:	November 30, 2013
Final Version due:	March 20, 2014
Tutorial proposal notifications:	Febuary 28, 2014
Main ABZ 2012 conference:

B 2012 - a FM2012 satellite workshop

**********************************************************************
                        DEADLINE EXTENSION

          Abstract submission: March 23, 2012
          Full paper submission: April 2, 2012

**********************************************************************


                         B 2012 - a FM2012 satellite workshop
                            Paris, France, August 28, 2012


http://membres-liglab.imag.fr/idani/B2012


OBJECTIVES

The B2012 workshop, co-located with FM, provides an opportunity to
widely gather the B community (from academia, industry and
administration). The idea is to cover an ample spectrum of topics, from
theoretical advances, tool support, industrial practice, new application
domains as well educational practice. It is also the place to hear about
recent advances in current industrial applications using B. Papers
discussing new ideas that are at an early stage of development are also
welcome.


INDICATIVE LIST OF TOPICS

Main topics addressed by the workshop are many, including but not
limited to:

• Theoretical advances : refinement, composition, code generation,
verification and proofs
• Modeling challenges, guidelines for formal development, integration of
B in software and
systems engineering
• Tool development, tool usage reports
• Case studies, return of experience, methodology, scaling up
• Teaching and training
• New perspectives

PAPER SUBMISSION

We invite two kinds of papers: long and short papers. Accepted long
papers will be published in ENTCS following the workshop.

• Long papers (10 ENTCS pages) dedicated to presenting research findings
in the identified topic areas of the workhop. Papers must describe
original work that does not substantially overlap with papers that have
been published or that are simultaneously submitted to a journal,
conference, or workshop with refereed proceedings.

• Short papers (max 6 ENTCS pages) dedicated to work in progress,
teaching experiments or case study. They do not constitute a refereed
publication. Hence, this will avoid any constraints on later publication.

Papers must follow the ENTCS guidelines
(http://www.entcs.org/prelim.html) and be submitted in PDF format and
will be handled via EasyChair
(https://www.easychair.org/conferences/?conf=b2012).


PROGRAM COMMITTEE :


Marie-Laure Potet -Vérimag – University of Grenoble – France (Chair)
Stefan Hallerstede - Aarhus University, Denmark(Co-chair)

Yamine Aït-Ameur, IRIT-ENSEEIHT, Toulouse, France
Christian Attiogbé, University of Nantes, France
Richard Banach, University of Manchester, IK
Michael Butler, university of Southampton, UK
Mamoun Filali, CNRS, University of Toulouse, France
Marc Frappier, Université de Sherbrooke, Québec, Canada
Stefan Hallerstede - Aarhus University, Danmark
Andrew Ireland, Heriot-Watt University, UK
Jacques Julliand, LIFC, University of Besançon, France
Régine Laleau, University of Paris-Est, France
Thierry Lecomte, Clearsy, France
Michael Leuschel, University of Düsseldorf, Germany
Anamaria Martins Moreira, UFRN, Natal, Brazil
Marie-Laure Potet, VERIMAG, University of Grenoble, France
Emil Sekerinski, McMaster University, Canada
Helen Treharne, University of Surrey, UK
Laurent Voisin, Systerel, France
Marina Waldén, Åbo Akademi University, Turku, Finland







-- 
Marie-Laure Potet
Prof. Grenoble INP

VERIMAG - Centre Equation
2 avenue de Vignate
38610 GIERES
FRANCE

Mail: Marie-Laure.Potet@imag.fr
Tel: +33 (0) 4 56 52 04 28
Fax:  +33 (0) 4 56 52 03 44

http://www-verimag.imag.fr/~potet

To reach us:
http://www-verimag.imag.fr/index.php?page=plan

ABZ 2012

http://ifm-abz.isti.cnr.it/page22/abzindex.html

B Track Chair :
Michael Leuschel , University of Düsseldorf, Germany (leuschel@cs.uni-duesseldorf.de)

FSEN '11

Fourth International Conference on 
Fundamentals of Software Engineering 2011 
Theory and Practice 
(FSEN '11) 

http://fsen.ir/2011/fsen.ir/2011 

Tehran, Iran 
April 20-22, 2011  

Workshop on B Dissemination

Workshop on B Dissemination

November 8-9, 2010
Natal, Brazil
http://www.bmethod.com/php/conference-sbmf-2010-en.php

Satellite event of SBMF 2010 <

http://sbmf2010.dimap.ufrn.br/>


    Presentation

This B / event-B workshop is organized on behalf of the 

DEPLOY project 
<http://www.deploy-project.eu/>. 

Its objectives are to present current 
status and ongoing research
and development related to B and 

event B languages and tools, as well as 
applications to industry size problems.
Topics addressed by the workshop are many,

including but not limited to:

* Tool development (language extensions,

external provers, code
generation, etc.)
* Modelling challenges (real time properties, probabilistic
refinement, design patterns, high order logic, etc.)
* Deployment (methodology, cases-studies, return of experience,
scaling up, etc.)
* Teaching and training

Researchers are invited to contribute to the

second day of the workshop 
through an open call for papers.


    Program

The workshop lasts 2 days:

* The first day is devoted to DEPLOY speakers. 

General presentation
of the project and tools will be sided by 

focused talks on
scientific/technical
matters (modelling time, code generation, 

model animation, model
checking, etc.) that are being researched in DEPLOY.
Reports on industrial applications (space, 

railways, automotive,
information systems, etc.) will complete the day.
* The second day is open to any presenter, 

through an international
 call for papers. Expected contributions would 

range from theoretical research to
practical applications of B/event B. 

Submissions are handled by
the programme committee.

The workshop is collocated with the SBMF

conference (Monday and 
Tuesday), at the Imira Plaza hotel &lt

;http://www.imiraplaza.com.br/>.


Important Dates
* Paper submission deadline: 30 July 2010
* Notification of acceptance/rejection: 

06 September 2010
* Workshop in Natal, Brazil: 08-09 November 2010


Submission and attendance

We anticipate a rich exchange of ideas and discussions 

during this event. Submissions are welcomed on any

subject that falls within the main issues.
Papers should be around 6 pages in ENTCS style.

All papers must be submitted in PDF format, 

following the instructions at the WOBD'10 submission 

site, handled by EasyChair:
http://www.easychair.org/conferences/?conf=wobd2010.

All accepted papers should be presented during the workshop.

Committees
 Workshop Chair:
* Thierry Lecomte <

mailto:thierry.lecomte@clearsy.com> (ClearSy)


 Program Committee:

* Michael Butler (University of Southampton, UK)
* Clif Jones (University of Newcastle, UK)
* Jérôme Phalampin (Siemens Transportation Systems, France)
* Lilian Burdy (ClearSy, France)
* David Basin (ETH Zurich, Switzerland)
* Michael Leuschel (University of Dusseldorf, Germany)
* Mathieu Clabaut (Systérel, France)
* Christophe Ponsard (CTIC, Belgium)
* Elena Troubitsyna (University of Turku, Finland)
* Rainer Gmehlich (Bosch, Germany)
* Aryldo Russo (AeS, Brazil)

3rd International Conference From Research to Teaching Formal Methods: The B Method (TFM-B'10)

First Call for papers
3rd International Conference
From Research to Teaching Formal Methods:
The B Method (TFM-B'10)
June 7, 2010,  Nantes, France
http://www.lina.univ-nantes.fr/apcb
------------------------------------------------
Invited Speaker:
Pierre Castéran / On Coq and B / 

LaBRI, U. Bordeaux
------------------------------------------------------

Overview: We anticipate a rich exchange of experiments

on research and teaching Formal Methods, in particular

the B method.
We would like to cover various works going from

the elaboration of courses till the teaching materials

and the evaluation of students and teachers 
themselves.

------------------------------------------------------

TOPICS: 
The topics of interest for TFM-B'2010 include but

are not limited to:
- Experiences with formal methods teaching using B
- Teaching materials for the B method
- Case studies and exercises featuring the B method
- The B method in the software engineering curriculum
- Use of the B method in disciplines other 

than software engineering
- New advances in the B method and their incorporation

into the teaching 
curriculum
- Tool supports for software engineering with the B method
- Teaching tool-equipped formal methods
- Teaching environments for model-based formal methods
- Combining the B method with other approaches
- Comparative studies on teaching formal methods
 . . .

------------------------------------------------------------------------------------
Important Dates:
Paper submission deadline            March 13, 2010
Notification of acceptance/rejection April 16, 2010
Final version of accepted papers     May   8,  2010
Workshop in Nantes, France           June  7,  2010
Proceedings with ISBN

-------------------------------------------------------------------------------------
Workshop Chairs:  Christian ATTIOGBÉ, 

Dominique MERY

Local Organization: COLOSS Team www.lina.univ-nantes.fr
LINA,  UMR CNRS 6241,  University of Nantes

Contact: bdays)@(univ-nantes.fr
http://www.lina.univ-nantes.fr/apcb

ABZ 2010

 ASM, Alloy, B and Z
Orford, Québec, Canada
February 22-25, 2010
http://abzconference.org/

The B International Conferences

• Conférence Z2B de Nantes (oct. 10-12 1995)
• Première conférence B de Nantes (nov. 25-27 1996)
• Deuxième conférence B à Montpellier (avril 22-24 1998),
• ZB'2000 à York (U.K.) 28 août, 2 sept. 2000),
• ZB'2002 Grenoble (F) (23-25 janv. 2002)
• ZB'2003, Turku (Finlande) (4-6 juin)
• ZB'05, Guildford (U.K.)
• B'2007 Besançon (France)
• B, from research to teaching, Nantes, (France), Cité Internationale des Congrès, 16 juin 2008
• ABZ Conference, September 16-18, 2008 BCS London Offices, Covent Garden, London,