From Research to Teaching Formal Methods - The B Method
TFM B'2010 (3rd edition)


>>   7 June 2010   <<
 Cité internationale
des congrès

Nantes  - France

Call for Papers [ .pdf file ]

Conférenciers invités/Invited speakers

Speaker : Pierre Castéran

Formal proofs of  local computation systems, using Rodin  and/or Coq

[slides] Abstract: PCbook
   This talk presents some work done at Loria and laBRI, in the framework of the {ANR RIMEL} project, and teaching distributed algorithmic.
    We first present a theoretical model called {Local Computations}, powerful enough to describe a wide class of distributed algorithms. Algorithm animation is done with the help of the {Visidia} tool.
    We present two ways to obtain {correct} local computation systems.  The first one is the construction by refinements, using the {Rodin} tool, starting from a formal specification, and ending with a model  that is compatible with the notion of local computation system. The other one consists in studying formally the main properties of  classes of local computation systems, and using these properties to prove the correctness of already written algorithms or show that some specifications are impossible to satisfy. This part is written with the {Coq} proof assistant.
    We present the main differences between these approaches and try to show how to make them cooperate. Finally, we show that distributed algorithmic and more specifically local computation systems can be used to revive the way of teaching important concepts as specification/realization, invariants, and program proving.

Speaker: Jean-Raymond Abrial

Development of a Network Topology Discovery Algorithm

[paper] [slides] Abstract:  PCbook
  Topology discovery is a distributed algorithm that is at the core of several routing algorithms, such as link-state routing. It is the problem of each node in the network discovering and maintening information on the network topology. The problem is challenging as the network can change rapidly, indeed more rapidly than the nodes can track and account for the changes. The topology discovery algorithm we develop generalizes of the "master and dog" paradigm. Here is the story. A master rides a motorbike while his dog, running behind him, tries to get to him. If the master reduces the speed of the motorbike, then the dog come a bit closer to him. However, if the master accelerates, then the distance between the two increases. But, certainly enough, if the master stops for a sufficiently long period of time then the dog will reach eventually his master.
   In our problem, the master is a graph representing the communication structure of a network. A move of the master corresponds to a modification of this graph. What makes our case different from the basic paradigm is that we have many dogs, each of them being a node in the graph. The distance between each dog and the master is represented by the difference between the physical graph and the image of it that each node constructs as soon as it gets some information about the "position" of the master. By definition, we say that a dog-node has reached the master-graph when the local image of the graph in this node corresponds exactly to the real situation of the graph...

Jean-Raymond Abrial is invited for the 2010 conference.  The new book of J.R. Abrial is announced for May, 2010.

Programme/Technical Program [proceedings]

8:30-9:00 Welcome

9h00 – 10h00 : Conférence invitée / Invited Talk

[slides] 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 

[slides] 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

[slides] Akos Fothi, Zoltan Istenès, Eötvös Lorànd University, HU [slides]

11h25- 11h40 Pause / Break

11h40 – 12h15 : New Features of Atelier B 4.0

[slides] Thierry Lecomte, ClearSy, Aix-en-Provence, FR 

12h15-12h50 : B for Children

[slides] Mireille Samia, St. Thaddeus Research, GE

12h50 – 14h00 : Déjeuner / Lunch

Visite de stands / Visit of stands

14h00 – 15h00 : Conférence invitée / Invited Talk

[paper] [slides] 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

[slides] Marc Guyomard, ENSSAT, Université de Rennes, FR

16h05-16h20 : Pause / Break

16h20 – 17h00 : Ten Years Disseminating the B Method,

[slides] Thierry Lecomte, ClearSy, Aix-en-Provence, FR