Tuesday, December 22, 2009

Software Specification Methods: An Overview Using a Case Study


1. Z – J. Bowen;
2. SAZ – F. Polack;
3. B – H. Diab and M. Frappier;
4. From UML Diagrams to B Specifications – R. Laleau and A. Mammar;
5. UML+Z: Augmenting UML with Z – N. Amalio, F. Polack and S. Stepney;
6. ASM – E. Börger, A. Gargantini and E. Riccobene;
7. TLA+ – L. Lamport; Part 2 - Event-Based Approaches
8. Action Systems – J. Sinclair;
9. Event B – D.Cansell and D. Méry

ABZ 2010

 ASM, Alloy, B and Z
Orford, Québec, Canada
February 22-25, 2010

Wednesday, November 25, 2009

Event-B and Rodin Documentation Wiki


This is the documentation wiki for the Event-b.org site providing documentation for users and developers of the Rodin toolset.
Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.
The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.

métro de Sao Paulo, Sao Paulo Metro

 November 2009,
We are delighted to announce the signing of a contract
with the Sao Paulo underground system for the development,
delivery and installation of the SIL3 COPPILOT security system, responsible
for controlling the opening and closing of the screen doors, which will be
installed on lines 2 and 3 of the Sao Paulo Metro...

Novembre 2009,
Nous avons le plaisir de vous annoncer la signature d'un contrat avec le métro de Sao Paulo pour le développement, la livraison et
l'installation du système sécuritaire SIL3 COPPILOT, chargé de la commande d'ouverture et de fermeture des portes palières qui vont être
installées sur les lignes 2 et 3 du Métro de Sao Paulo...

Message de Clearsy

Sunday, August 2, 2009

Rodin workshop

The Rodin workshop took place last week and
abstracts and slides are available on the Event-B wiki:


A follow-on workshop will be held next summer.
Date and venue to be decided.

Michael Butler

On 21/05/2009 15:39, "Michael J Butler"
<mjb@ecs.soton.ac.uk> wrote:

A reminder about the Rodin Developer Workshop
in Southampton in July 2009:


Note that we have now decided to hold
a 1-day tutorial on Rodin plug-in
development on 15 July just before
the workshop. The tutorial is intended
for existing and prospective plug-in
developers. It will give an overview
of the architecture of Rodin and
provide guidance on building plug-ins.


Michael Butler, University of Southampton
Stefan Hallerstede, Heinrich-Heine-Universität Düsseldorf
Laurent Voisin, Systerel

Formal Methods Week


conference workshop: recent innovations and applications in B


Tuesday, June 9, 2009

Conférence grand public : le réchauffement climatique

Vincent Courtillot, J.M. Salles, J. Girardeau et le présentateur.
Le discours opposé à celui de Vincent Courtillot se trouve par exemple ici
Une pétition citée par V. Courtillot est ici

Conference : programme

8:30-9:00 Welcome

9:00-10:00 Invited Conference

Prof. Michael Leuschel, University of Düsseldorf details

10:00-10:15 Break

10:15-11:00 Latest News on AtelierB V4

Antoine Requet, ClearSy, France details

11:00-11:35 Sculpturing Event-B Models with Rodin: Holes and Lumps in Teaching Refinement through Problem-Based Learning

J. Paul Gibson, Eric Lallet, Jean-Luc Raffy, Telecom& Management SudParis, France

11:35-11:50 Break

11:50-12:25 Teaching the B Method at Oxford Brookes

D. Lightfoot, C. Martin, Oxford Brookes University, UK

12:25-13:00 Twelve Years of B Teaching in an Engineer School : from a Correct by Design Approach to Analysis Techniques and Tools

M-L. Pottet, Verimag Grenoble, France

13:00-14:00 Lunch

14:00-14:35 High-Level versus Low-Level Specifications: Comparing B with Promela and ProB with Spin

Mireille Samia, Harald Wiegard, Jens Bendisposto, Michael Leuschel, University of Düsseldorf, DE

14:35-15:10 BiCoax, a Proof Tool Traceable to the BBook

Samuel Colin, George Mariano, INRETS, France

15:10-16:15 Break - Demos

16:15-16:50 Constructing a Formal Event Model of Linux File System Access Permissions: A Research-Based Teaching Approach

David Cumbor, Bill Stoddard, University of Teesside, UK

16:50-17:25 How to make mistakes?

Stefan Hallerstede, University of Düsseldorf, DE

17:25-18:00 To structure, Realize and Prove: How and Why

Alain Couturier(1), Michel Gazeau(1), Gérald Jean-Baptiste(1), Gwenola Kerglonou(2), (1) CNAM Pays-Loire and (2) ICAM Nantes, France

Conference June 8-2009

The invited conference of Prof. Michael Leuschel, University of Düsseldorf, and the conference of J. Paul Gibson.
The public of the conference.

Friday, June 5, 2009

Royal de Luxe. The giants are in the city ! Programme

More pictures HERE

Vendredi 5 juin : La petite géante devrait se réveiller vers 11h place Viarme et le scaphandrier géant devrait émerger du bassin Saint-Félix vers 13h30 au niveau du pont Tbilissi. Ils parcourront ensuite les rues de Nantes le vendredi après-midi (chacun de leur côté ou ensemble ?) : le scaphandrier devrait atteindre la place de la petite Hollande vers 15h avant de se reposer. Le spectacle reprendra ensuite vers 19h.

Samedi 6 juin : Un réveil est prévu samedi 6 juin à partir de 10 h au niveau du château (à proximité des loups en liberté dans les douves).

Dimanche 7 juin : Ils embarqueront à bord d’un chaland vers 11h à proximité du pont Anne de Bretagne (et donc du grand éléphant :-). Le bel équipage naviguera en direction de Saint-Nazaire via Indre, Couëron, Le Pellerin, Frossay et Paimboeuf. L’arrivée à St-Nazaire est prévue vers 17 h et la fin du spectacle, en début de soirée vers 20h/20h30.

Photos taken this morning (5-06-2009, 11h 30)

Wednesday, May 20, 2009

Monday, May 18, 2009

From the Airport/Train Station to the Cité des Congrès

The Cité des Congrès is very close to the Railway Station (Gare TGV, sortie Sud) (don't use a taxi or a public transportation). The Gare TGV sortie Sud is also the stop of the airport shuttle (navette aéroport TAN).

The City of Congress brings you the Cité pass ( City Pass) allowing access to the entire public transportation network of Nantes ( TAN) , including airport shuttles. The Cité Pass is valid only on Monday, June 16, 2008. If you wish to receive the Cité Pass please ask us before your arrival at Nantes.

From the airport Nantes Atlantique to Nantes

You can use (with the cité pass). Ask your FREE Cité pass to use the public transportations :

  • the airport shuttle (tanair), Bus, 19 minutes
  • a bus connected to the tramway (tan) :

- Bus n° 37, Direction Croix Jeannette, Arrêt (stop) Neustrie

- then Tram 3, direction Sillon de Bretagne, Arrêt (stop) Commerce. Here you will find a lot of buses and tramways

Tuesday, May 12, 2009

"Data Semantics"

Two pages of Data Semantics, J.R. Abrial, IFIP WC on Data Base Management, Cargèse, Corsica, France, 1-5 April 1974,
Proceedings edited by J.W. Klimbie and K.L. Koffeman, North-Holland

Specification or how yo make Abstraction Real

Click on the image to enlarge it.

TSI, vol. 3, n° 3, 1984
The two first pages. To read the entire paper go here

Yes, you are in Nantes !

Ile de Versailles (Japon) et Parc du Grand Blottereau (Corée)

Saturday, May 9, 2009

During the Journées Scientifiques 2009

2 conférences grand public :

"Le réchauffement climatique" par Vincent COURTILLOT ;

"Peut-on donner une valeur marchande à la biodiversité ?" par Jean-Michel SALLES,

Bienvenue à Nantes, la ville où le monde se retrouve !

Royal de Luxe, Nantes.
June 7-2009, Do not miss Royal de luxe !
Enjoy the B Conference to follow the free show by Royal de luxe!

in Nantes!

Bine ati venit la Nantes !
Benvenuti a Nantes
Καλώς ήρθατε στην Ναντ !
Bem-Venido a Nantes
Failte go Nantes
Welcome to Nantes
Welkommen til Nantes
Willkommen in Nantes
مرحبا بكم في نانت
Добро пожаловать в Нанте!

Friday, May 8, 2009

Read the archives 2008

you will find information on transportation, hostels, etc.

Le Trois-Mâts Belem à Nantes

Le Trois-Mâts, construit et lancé à Nantes en 1896, se visite les 6 et 7 juin 2009. Il est l’un des plus anciens grands voiliers naviguant au monde.
France's only remaining three masted barque, one of the oldest tall ships still sailing the seas...


The web site

Your public transport itineraries



Destineo calculates your public transport itineraries in the Pays de la Loire region.

Visit Nantes, Guérande, Saumur or Les Sables d’Olonne by bus, coach or train!

You can also find out about hotels and restaurants that are accessible by public transport.
hotels and restaurants

June 7-2009, Nantes, Royal de Luxe

Du 5 au 7 juin 2009, Royal de Luxe revient avec un nouveau spectacle de géants dans le cadre de la biennale d'art contemporain Estuaire 2009.


Royal de Luxe are an extraordinary European street theatre company, renowned on three continents but hardly known in Britain.

The director Jean Luc Courcoult founded the company in 1979, and they have performed all over the world ever since.

The company has visited countries all over Europe as well as Korea, China, Vietnam, Chile and Africa. Some of their most celebrated shows – including La véritable histoire de France, Roman photo tournage and Le péplum have been revived many times and performed in front of thousands of spectators. They spent six months in Africa and three in China

In the past dozen years, they have created a series of spectacular shows involving giant figures as big as 11 or 12 metres high. Shows are simple – the animal or giant arrives in town and lives its life, going about its business for a few days. Extraordinary interactions take place between passers-by and the performance; residents become enchanted with the activities of these miraculous beings and begin to follow their every move. By the end of the performance, huge crowds gather daily to watch the latest episode in the life of the visiting creature. The Sultan’s Elephant is the fifth in the series of giant pieces, the others being Le Géant tombé du ciel, Le géant tombé du ciel: dernier voyage, Retour d'Afrique and Les Chasseurs de girafes.

La visite du sultan des Indes sur son éléphant à voyager dans le temps was first performed in Nantes from May 19th to 22nd and in Amiens from June 16th to 19th 2005, on the occasion of the centenary of Jules Verne's death. This production was commissioned by the cities of Nantes and Amiens and has received a special grant from the Ministry of Culture and Communication."

source :


In English : http://en.wikipedia.org/wiki/Royal_de_luxe
(Pour l'heure, c'est top secret! et voulu car comme d'habitude, il convient de préserver une part de mystère autour de cette nouvelle création qui s'appuie sur un fabuleux conte pour petits et grands...).

Photos Here

Fête d’ouverture
Royal de Luxe
“La géante du Titanic et le scaphandrier”*

Vendredi 5, samedi 6 et dimanche 7 juin

Estuaire 2009 signe le retour d’une nouvelle création de la compagnie de théâtre de rue Royal de Luxe. Pendant trois jours, Jean-Luc Courcoult, auteur et metteur en scène, nous fait partager de nouveaux moments de vie du Géant et de sa nièce, la Petite Géante.
Et comme la Loire est le personnage principal de notre aventure estuarienne, préparez-vous à de nombreuses surprises… Notamment le dimanche 7 juin : prévoyez pique-nique, vélos et canoës pour nous accompagner sur les bords du fleuve !

“En 1912 coulait le Titanic. Mais ce que l’histoire n’a pas retenu c’est qu’il transportait en secret une géante de 10 m de hauteur, capturée dans la Terre des glaces, à l’époque gouvernée par le Danemark. L’Islande, faite de volcans, abritait alors certains géants fort occupés à moduler le paysage pour en faire une terre habitable. L’un d’entre eux, ou plutôt l’une d’entre elles, avait pour tâche de faire apparaître d’immenses geysers destinés à correspondre d’une montagne à l’autre : un peu comme les Indiens d’Amérique avec leurs nuages de fumée, ou l’invention du sémaphore à la Révolution française.

Des corsaires anglais, au solde de sa Majesté, capturèrent la géante. Elle fut embarquée clandestinement dans une cale du Titanic afin d’être exhibée dans le Nouveau Monde et démontrer ainsi la suprématie du Royaume-Uni. Comme chacun sait, le navire déchiré par un iceberg venant du Nord de l’Islande, sombra et par le fait notre géante avec. Mais comme tout passager du bâtiment notre géante avait de la famille : un frère nommé “le géant” et une fille appelée “petite géante”. Pendant la capture de sa mère, la petite géante s’enfuit sur un bateau. Le géant, occupé à scier des icebergs constata à son retour la disparition de ses amis. Durant de longues années, il parcourut le fond des océans et finit par retrouver l’épave. Il enterra sa sœur au fond de la mer et découvrit la malle-poste du paquebot gisant à quelques centaines de mètres de la carcasse brisée. Alors il décida de distribuer le courrier du vaisseau mythologique et de rejoindre sa nièce : la petite géante.”

Jean-Luc Courcoult


My pictures on Royal de luxe :
Royal de Luxe à Nantes en octobre 2001 Petits contes chinois revus et corrigés par les nègres

2005, the Elephant

Programme of the 2009 Conference


Thursday, March 26, 2009

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

Sunday, March 15, 2009

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
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
Specialist in Safety Critical Systems

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.

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.


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.

[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/

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

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


Wednesday, January 14, 2009

BWW, B World Wide


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.