Formal Methods Wiki

I have created a new Formal Methods Wiki under
http://formalmethods.wikia.com . This includes new versions of the Virtual  Library forma methods pages, that are unfortunately now offline due to a disk error.
These pages are now editable by anyone, so I am hoping that members of the formal methods community will improve these and bring them up
to date, as well as adding new formal methods-related material.

The facility is based on Wikia, established by Jimmy Wales who also founded  Wikipedia. The underlying wiki software is MediaWiki, the same as Wikipedia.
I would encourage all members of the formal methods community to contribute  any information related to formal methods to the wiki, including hyperlinks
to further information. It is best although not essential to register with  the site if you plan to do more that a small number of edits. This is very
simple (similar to Wikipedia). If you are unsure of the MediaWiki markup, it  is easiest to press the "Edit" button on a page that is similar to one you
wish to create, copy the text, paste it into the new page, and edit it as  required.

I hope this facility is helpful. Please don't worry about making mistakes  since everything is easily correctable on a wiki; I will keep an eye on new
entries and edit further as needed. I look forward to your active  participation on the site!

--
Prof. Jonathan P. Bowen, Emeritus Professor, London South Bank University
Faculty of BCIM, Borough Road, London SE1 0AA, UK
Visiting Professor, King's College London
Email: jonathan.bowen@lsbu.ac.uk  URL: http://jpbowen.googlepages.com

User Manual of B Language , Redaction Guide of Mathematic Rules

Deux nouveaux manuels dédiés à l'Atelier B sont désormais disponibles :
- Manuel Utilisateur du Langage B
- Guide de Rédaction de Règles Mathématiques
              
Ces derniers sont actuellement en français et disponibles en open-source (licence Creatice Commons - Paternité). Nous recherchons actuellement des traducteurs souhaitant réaliser
la traduction en anglais de ces 2 documents.
              
Pour participer à ce projet, merci de nous contacter à l'adresse suivante : contact@atelierb.eu.
Bien cordialement
CLEARSY SYSTEM ENGINEERING
Spécialiste des Systèmes Sécuritaires
              
              
Dear Users,
              
Two new manuals dedicated to Atelier B are now available :
              
User Manual of B Language
Redaction Guide of Mathematic Rules
              
              
These manuals are available in french and released as open-souce (License Creative Commons - Attribution). We are currently searching for translators wishing to
contribute to english translation of these 2 documents.
              
To participate to this work, please contact us: contact@atelierb.eu.
Best Regards
CLEARSY SYSTEM ENGINEERING
Specialist in Safety Critical Systems

"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.

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

BWW, B World Wide

http://www.methode-b.com/images/carte_b.jpg

The beta 2 version of Atelier B 4.0

              
Starting with the launch of the beta 2
 version of Atelier B 4.0, which is
now available at no cost on the Atelier
 B site in order to collect opinions
and comments, then finalize a stable
 version by the end of January 2009.
         

Une application de B

Le système COPP qui permet l'ouverture et la fermeture des Portes Palières installées sur la station de métro Porte de Châtillon à Paris a été officiellement mis en service en août 2008.
http://www.copp.fr/php/presentation_copp_fr.php