"Extending B without changing it"

J.R. Abrial, Extending B without changing it (for developing distributed systems)
file:///U:/public_html/ConfZetBdeNantes/Abrial.htm

Atelier B or Atelier B ?

What's in a name?

http://atelier-b.blogspot.com/
http://www.atelierb.eu/html/liens.html

Une introduction à la méthode B

http://www.sciences.univ-nantes.fr/info/perso/permanents/habrias/methodb.html

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:

https://gna.org/projects/brillant

where this project is hosted, in a "bicoax" subdirectory of the Subversion trunk.

http://download.gna.org/brillant/snapshots/ 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.

http://download.gna.org/brillant/snapshots/bicoax-html/
and
http://download.gna.org/brillant/snapshots/bicoax-html/toc.html

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:
http://download.gna.org/brillant/snapshots/BiCoax-announce
with more technical details.

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

References:
[1] http://coq.inria.fr/
[2] http://en.wikipedia.org/wiki/B-Method
or http://fr.wikipedia.org/wiki/Méthode_B
[3] http://books.google.com/books?id=Cbx9A85TrOYC
only excerpts are available, but a lot of chapter 2 is visible

--
Samuel Colin
E-mail: scolin@hivernal.org
Informations: http://hivernal.org/static/about/

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

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

                 Conference
From Research to Teaching Formal Methods - The B Method
                     TFM B'2009
         8 June, 2009,  Nantes, France
              www.lina.univ-nantes.fr/apcb
          
==================================================

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
teaching.
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)
www.lina.univ-nantes.fr/apcb/


Organization and Contact:
COLOSS Team
bdays@univ-nantes.fr


Overview:
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.

TOPICS:
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
www.springer.com/computer/lncs?SGWID=0-164-7-72376-0


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 bdays@univ-nantes.fr with the subject "TFM_B Submission".

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

=======================================================