Sunday, December 12, 2010

Tuesday, November 30, 2010

Structures de données et méthodes formelles, Marc Guyomard, Springer

Ce livre porte sur l’étude des structures de données, à savoir des constituants logiciels dont la qualité conditionne le bon fonctionnement et l’efficacité des applications informatiques. L’originalité de cet ouvrage réside essentiellement dans le lien qu’il établit avec la discipline des méthodes formelles pour le génie logiciel. Il montre comment il est possible de calculer les opérations qui accompagnent une structure de données à partir d’une spécification rigoureuse. L’auteur adopte à la fois une perspective historique et une démarche fonctionnelle. La première partie de l’ouvrage présente les bases de la discipline : la théorie des ensembles, l’étude de structures intermédiaires (listes, arbres, sacs), et l’analyse des algorithmes. La seconde partie se focalise sur l’étude approfondie de cinq structures de données typiques : les ensembles simples, les ensembles composites, les files simples, les files de priorité, et les tableaux flexibles. Des exercices accompagnent chaque chapitre.

1st Edition., 2011, 426 p., Broché
ISBN: 978-2-8178-0199-5

Monday, November 29, 2010

Décès de Michel Sintzoff

On m'apprend :

" C'est avec une très grande tristesse que j'ai appris ce lundi le décès de Michel Sintzoff.
Michel était une personnalité exceptionnelle de la recherche en Informatique. Sa curiosité scientifique l'avait amené à travailler dans de nombreux domaines de notre discipline (Langages, Intelligence Artificielle, Bases de Données, Génie Logiciel, Informatique Distribuée,...).

Il avait des amis partout dans le monde, et donc naturellement en France (à Paris, Toulouse, Nancy, Grenoble,...).Beaucoup se souviendront de son ouverture d'esprit, de la pertinence de ses remarques et de son rire inimitable. "

Wednesday, October 20, 2010

FSEN '11

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

Tehran, Iran 
April 20-22, 2011  

The Space and Motion of Communicating Agents

Robin Milner, Cambridge, 2009

Cours et exercices corrigés d'algorithmique

Vérifier, tester et concevoir des programmes en les modélisant,
Jacques Julliand
Vuibert, 2010

Utilise la notation B.

Death of Jean-Claude Laprie

Dear colleague,

With deep sadness we bring you the news of Jean-Claude
passing away after a battle with cancer, 
Saturday night (October 17).
The funeral arrangements are not settled yet. 
More information will be provided when

TSF group at LAAS

Thursday, October 7, 2010

Méthodes de spécification de systèmes temps réel en B


"B is a computer language designed by D. M. Ritchie and K. L.
Thompson, for primarily non-numeric applications such as system
programming. These typically involve complex logical decisionmaking,
and processing of integers, characters, and bit strings.
On the H6070 TSS system, B programs are usually much easier to
write and understand than assembly language programsj and object
code efficiency is almost as good. Implementation of simple TSS
subsystems is an especially appropriate use for B."

B vs. Coq to prove a Garbage Collector

Processus de validation basée sur la notion de propriété

Formal Methods in Safety-Critical Railway Systems

Vers une méthodologie de Validation et de Vérification multi-formelle des Interfaces Utilisateurs en milieu industriel

The Development of a Probabilistic B-Method and a Supporting Toolkit

Les bases du langage B

A formal specification of the javaByte code semantics using the B method

Using B Method to Formalize the Java Card Runtime Security Policy for a Common Criteria Evaluation

How to formally specify the Java Bytecode semantics using the B method

Formalisation and Veri¯cation of the GlobalPlatform Card Speci¯cation Using the B Method

ProB: An Automated Analysis Toolset for the B Method

Applying the B Formal Method to the Bossa Domain-Specific Language

Cooperation Between the B Method and the Automata Theory to Check the Component Interoperability

PBS, support of the B Method in PVS, Cesar Munoz, SRI

Component-based Development using the B method

Tutorial on the B method

The B Method for Programmers

The formal method known as B and a sketch for its implementation

Antti-Juhani Kaijanaho
Master's Thesis
in Information Technology (Software Engineering)
20th December 2002

Program Development by Refinement: Case Studies Using the B Method (Formal Approaches to Computing and Information Technology (FACIT))

Emil Sekerinski (Editor), Kaisa Sere (Editor)

Security of Computer Architectures, Jean-Louis Boulanger

Le dernier livre d'Umberto Eco en français 

Dall'albero al labirinto. Studi storici sul segno e l'interpretazione 

Studi storici sul segno e l’interpretazione

Autore: Umberto Eco  
Titolo: Dall'albero al labirinto. Studi storici sul segno e l'interpretazione  
Editore: BOMPIANI 
Pagine: 640 
Prezzo: 25,00 euro  
Anno prima edizione: 2007  
ISBN: 45259029

FM 2011 (20-24 June 2011, Limerick, Ireland): Call for Tutorials

Tuesday, June 15, 2010

Workshop on B Dissemination

Workshop on B Dissemination

November 8-9, 2010
Natal, Brazil

Satellite event of SBMF 2010 <>


This B / event-B workshop is organized on behalf of the 
DEPLOY project 
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.


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

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:

All accepted papers should be presented during the workshop.

 Workshop Chair:
* Thierry Lecomte <> (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)

Tuesday, June 8, 2010

B方法 , The B Book in chinese


General-Service Ballistic Computer Programming Based on B-Method

"Formal methods offer the promise of significant improvement on quality and reliability of critical embedded software. B-Method is employed to develop general-service ballistic computer programs in the paper, each of which can be adapted to a family of service/weapon-specific ballistic computers. Based on the structuring mechanisms of B-method, a unified approach is proposed to systematically control the complexity of ballistic parameters in the process of type and operation refinement, and ultimately a series of high reliable, reusable, and scalable programs are produced. Experiences with the application of the method and tools are also discussed."

Formal development of a washing machine controller by using formal design patterns

Event Model Decomposition

The papers and the slides of the conference 2010 are here ...

Sunday, May 9, 2010

On line registration for the 2010 Conference

Programme of the 2010 conference

8:30-9:00 Welcome

9h00 – 10h00 : Conférence invitée / Invited Talk
Formal proofs of local computation systems, using Rodin and/or Coq
Pierre Castéran, Université de Bordeaux, LaBRI, FR
10h00 – 10h15 : Pause / Break

10h15 – 10h50 : Teaching Logic Proofs for Formal Aspects
David Cumbor, Bill Stoddart, Steve Dunne, University of Teesside, UK
10h50 – 11h25 : Using the B Method in Teaching Software Technology at Eötvös Lorànd University
Akos Fothi, Zoltan Istenès, Eötvös Lorànd University, HU

11h25- 11h40 Pause / Break

11h40 – 12h15 : New Features of Atelier B 4.0
Thierry Lecomte, ClearSy, Aix-en-Provence, FR

12h15-12h50 : B for Children
Mireille Samia, University of Dusseldorf, GE

12h50 – 14h00 : Déjeuner / Lunch
Visite de stands / Visit of stands

14h00 – 15h00 : Conférence invitée / Invited Talk
Development of a Network Topology Discovery Algorithm
Jean-Raymond Abrial, Consultant, Marseille, FR
15h30 – 16h05 : The Teaching of Data Structures: a Balanced Presentation of Skew Heaps
Marc Guyomard, ENSSAT, Université de Rennes, FR
16h05-16h20 : Pause / Break

16h20 – 17h00 : Ten Years Disseminating the B Method,
Thierry Lecomte, ClearSy, Aix-en-Provence, FR

Friday, April 30, 2010

Jean-Raymond Abrial, conference in Nantes on June 7, 2010

Jean-Raymond Abrial is invited for the 2010 conference.  The new book of J.R. Abrial will be available for the conference.


Prologue: faultless systems – yes we can!; Acknowledgements; 1. Introduction; 2. Controlling cars on a bridge; 3. A mechanical press controller; 4. A simple file transfer protocol; 5. The Event-B modeling notation and proof obligations rules; 6. Bounded re-transmission protocol; 7. Development of a concurrent program; 8. Development of electronic circuits; 9. Mathematical language; 10. Leader election on a ring-shaped network; 11. Synchronizing a tree-shaped network; 12. Routing algorithm for a mobile agent; 13. Leader election on a connected graph network; 14. Mathematical models for proof obligations; 15. Development of sequential programs; 16. A location access controller; 17. Train system; 18. Problems; Index.

Saturday, April 3, 2010

Conférences grand public JS 2010

L'un des objectifs des Journées Scientifiques de l'Université de Nantes est de diffuser la culture scientifique et technique.

Cette année, le thème de l'enfant et son éducation est à l'honneur.

Les conférences et la table ronde programmées sont gratuites et accessibles à tous.

Programme prévisionnel

  • 15h00-15h45 : Conférence « Comment la connaissance vient aux bébés » par Roger LÉCUYER, Professeur émérite en psychologie de l'enfant, à l'Université Paris V, spécialiste des compétences périnatales

  • 16h00-16h45 : Conférence « Stratégies familiales et politiques éducatives » par Agnès VAN ZANTEN, directrice de recherche au CNRS, à l'Observatoire Sociologique du Changement

  • 17h00-18h00 : Table ronde sur le thème de l'enfant et son éducation avec Roger LÉCUYER, Agnès VAN ZANTEN, Jean-Christophe ROZÉ (Chef du service de médecine néonatale au CHU Nantes), Catherine CHOQUET (Adjointe au maire de Nantes en charge de la petite enfance, de la santé et des personnes handicapées) et Agnès FLORIN (Professeur en Psychologie de l'enfant et de l'éducation à l'Université de Nantes)

Tuesday, March 30, 2010

Death of Robin Milner

"Robin Milner, FRS FRSE
Professor Emeritus of Computer Science
It is with great sadness that we note the death of Robin Milner.
Robin worked at the Computer Laboratory in Cambridge from 1995 onwards, serving as Head of the Laboratory 1996–1999. Before that, he worked at the University of Edinburgh 1973–1994, where he was founding Director of the Laboratory for Foundations of Computer Science (LFCS). He was awarded the Turing Award in 1991.
Robin played a leading role in the development of many areas of Computer Science, focussing especially on its mathematical foundations but always with a sharp eye on practice. His intellectual legacy includes:
  • machine-assisted proof construction with the LCF approach, underpinning the HOL and Isabelle/HOL provers;
  • the design and formal definition of programming languages, especially of Standard ML, including work on type safety, type inference and module systems;
  • models of concurrent computation, particularly with the CCS and Pi-Calculus process calculi and their theories of compositional reasoning; and
  • the bigraph model of mobile informatic processes with its applications to bioinformatics and pervasive computing.
These provide the basis and tools for a great deal of current research, by many people worldwide.
Always an inspirational teacher and colleague, and a warm-hearted man, he will be greatly missed."

Robin Milner visited Nantes on 2007 for a conference.

Saturday, March 20, 2010

Invited Speaker 2010

3rd International Conference
From Research to Teaching Formal Methods:
The B Method (TFM-B'10)
June 7, 2010,  Nantes, France
Pierre Castéran 

Commandes latex pour B, Latex commands for B

Nous donnons le code ASCII et en face la commande Latex
  • : \in
  • /: \notin
  • <: \subseteq
  • /<:
  • ><
  • => \implies
  • % \lambda
  • ; \comp
  • \/ \cup
  • /\ \cap
  • & \land
  • or \lor
  • ! \forall
  • # \exists
  • --> \fun
  • +-> \pfun
  • >--> \bij
  • <--> \rel
  • |-> \mapsto
  • |> \rres
  • <| \dres
  • ||> \nrres
  • <|| \ndrres
  • >+-> \pbij
  • +->> \psurj
  • >+-> \pinj
  • -->> \surj
  • >--> \inj
  • == \defs
  • <-- \leftarrow
  • || \parallel
  • /= \neq
  • <= \leq
  • {} \emptyset
  • * \times (produit cartésien, cartesian product)

Monday, March 1, 2010

B in Brazil

Sacomã station in Sao Paulo is now equipped with the COPPILOT System
Since January 10 2010, the new Sacomã station (Line 2 - green) in Brazil
 is open to the public since its inauguration by Governor Jose Serra in  Sao Paulo..

Monday, February 1, 2010

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

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 
- 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
LINA,  UMR CNRS 6241,  University of Nantes

Contact: bdays)@(

Wednesday, January 20, 2010

"A genius writes code an idiot can understand, while an idiot writes code the compiler can't understand. " (Anon )

Investigation into the teaching of B worldwide

Investigation into the teaching of B worldwide

  The Questionaire
Where is B taught  ?
We would like to update the investigation carried out over a year ago by Marie Laure Potet.
Please fill in the following questionaire and return it to us.

University: B is taught in the following departments, on the following courses,
in the following years:
[So we can store as triples (Department, Course, year)]
Department: (E.g. Computer Science)
Course: (E.g. BSc Computer Science)
Year: (E.g. 1st, 2nd)
Duration of Course in lecture hours (e.g. 20 hours)
Do you use a tool? (If so which one?):
How long do the students spend using the tool in the lecturers presence?: (E.g. 20 hours)
Is B used in assignments (outside normal teaching hours)?:
What is the relation between the teaching of B and the teaching of mathematics and logic for IT:
Under which discipline is B taught (e.g. software engineering, programming etc.):
Name of course contact:
Email address:
Type of assessment (e.g. supervised project, group project, machine-based exam):
Have you written course notes?:
Would you be prepared to share them with colleagues?:
The responses to this questionaire have been provided by:
First Name:
Postal Address:
E-mail Address:
They are correct as of the date:
Please circulate to other interested parties.
H. Habrias.
We will send an analysis of the results of the questionaire to everyone who has filled one in.
The information provided will be available from one or several web sites. If you do not want your information to be made publicly
available then please do not provide it.
We abide by the freedom of information act.
Completed questionaires (and any questions) should be addressed to:
Henri Habrias
henri dot  habrias  at univ-nantes dot fr

The answers (2002 !)

Monday, January 4, 2010

Modeling in Event-B

Modeling in Event-B
System and Software Design
Jean-Raymond Abrial
Swiss Federal University (ETH), Zürich
 (ISBN-13: 9780521895569)
Not yet published - available from June 2010
 (Stock level updated: 12:41 GMT, 04 January 2010)
c. £60.00