Wednesday, February 18, 2009

"Extending B without changing it"

J.R. Abrial, Extending B without changing it (for developing distributed systems)

Atelier B or Atelier B ?

What's in a name?

Une introduction à la méthode B

and some pages on B

a shallow embedding of B set-theory in Coq

A message of Samuel Colin
Hi list,
for the past months I spent some effort upon the development of a shallow embedding of B set-theory in Coq[1]. The goal was two-fold:
- Validate, by implementing them, theorems of the B-Book, the "bible" of the B method[2]
- Have a prover for B based on what is described in the B-Book[3]

So, firstly, some links:

where this project is hosted, in a "bicoax" subdirectory of the Subversion trunk. for tarballs (you want the most recent one)
It should compile on a Linux platform with coq 8.2 (available as of very recently) and make, see the INSTALL file.

for the documentation generated by coqdoc (most of the comments refer to the place in the BBook of the corresponding theorem/definition).

In a nutshell and very broadly, I make this announce because it has entered a usable state, as showed by the Bmisc.v file of the project, containing two examples of small B projects whose all proof obligations are proved in BiCoax. BiCoax will be (and is already, in a sense) plugged back into the other tools of the BRILLANT platform so as to obtain a full toolchain for developing B projects.

What is implemented covers the first part of the B-Book: the first chapter (logical connectors), the second chapter (derived constructs, relations, functions) and half of the third chapter (mathematical constructs, up to and not including relative integers). Some constructs introduced in event-B were also added and I also put some eventB unicode notations with (hopefully) the correct priority as described by the Rodin D7 deliverable.

You can find an expanded version of this message here:
with more technical details.

This message was sent to the "BForum" mailing-list and the "Coq-club" mailing list.

only excerpts are available, but a lot of chapter 2 is visible

Samuel Colin

Thursday, February 12, 2009

***Call for papers*** From Research to Teaching Formal Methods - The B Method

***Call for papers***

From Research to Teaching Formal Methods - The B Method
TFM B'2009
8 June, 2009, Nantes, France


The first B conference took place in Nantes during November 1996
and was followed by the Montpellier, York, Grenoble, Turku,
Guilford and Besancon, and London (2008) Conferences.
During the conferences of Montpellier and Grenoble,
education sessions were held with published proceedings.
The APBC Association (International B
Conferences Steering Committee) organised meetings
in Paris and in Nantes. The
Nantes meeting was devoted to teaching. But since a
few years, there was no meeting dedicated to
Software Engineering research must lead to put
it into practice. For that, it is
necessary to use teaching, teaching that must
conciliate the basics and the practice.
We may consider two principal arguments in favour
of teaching the B method:
First, the B method and his concepts can be
considered as having an essential pedagogical
interest even if this method is not used.
The B method is an industrial method which
reaches the industrialisation level going
from specification to programming. There
are several examples of concrete applications.
In this 2009 edition we also encourage the
submission of papers describing teaching
experiments based on other tool-equipped
formal methods that are used in industry
and that help in adopting formal methods
in curricula.

**********Call for papers***********

From Research to Teaching Formal Methods:
The B Method

Workshop Chairs:
Christian ATTIOGBÉ,
Dominique MERY

Program Committee (under construction):

Christian ATTIOGBE, [Chair], University of Nantes, France
Rueda Camilo, Universidad Javeriana-Cali, Colombia
Lars-Henrik ERIKSSON, Uppsala Universitet, Sweden
Marc FRAPPIER, Sherbrooke, Canada
Marc GUYOMARD,Rennes, France
Henri HABRIAS, University of Nantes, Fance
Jacques JULLIAND, University of Besançon, France
Michael LEUSCHEL, University of Düsseldorf, Germany
Dominique MERY, LORIA, Nancy, France
Mike POPPLETON, University of Southampton, UK
Ken ROBINSON, Univ. of New South Wales, Australia
Emil SEKERINSKI, McMaster University, Ontario, Canada
Elena TROUBITSYNA, Abo Akademi University, Finland
Zoltan ISTENES, Elte University, Hungary

Local Organization:
COLOSS Team (LINA Nantes)

Organization and Contact:

We anticipate a rich exchange of experiments
on 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.

The topics of interest for TFM B'2009
include but are not limited to:

- Teaching tool-equipped formal methods
- Teaching environments for the B method
- Teaching environments for model-based formal methods
- The B method in the software engineering curriculum
- Tool support for software engineering with the B method
- Experiences with FM teaching using B
- Combining the B method with other approaches
- Comparative studies on teaching formal methods
- Case studies and exercises featuring the B method
- Use of the B method in disciplines other
than software engineering
- New advances in the B method and their
incorporation into the teaching curriculum

Important Dates:
Paper submission deadline: 20th March 2009
Notification of acceptance/rejection: 24 April 2009
Final version of accepted papers: 8 Mai 2009
Workshop in Nantes, France 8 June 2009

Submission and Attendance:

Papers must be written in English and must not exceed
15 pages.
LNCS-style templates are available at

Papers must be submitted by 20 March 2009 by email
with an abstract
in plain text and the paper itself as a PDF attachment,
to with the subject "TFM_B Submission".

All accepted papers should be presented during the
1-day workshop.