TFM B'2010 (3rd edition)

Nantes - France Call for Papers [ .pdf file ] |

- Pierre Casteran
- Jean-Raymond Abrial

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.

http://www.labri.fr/perso/casteran/CoqArt/index.html

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.

http://www.labri.fr/perso/casteran/CoqArt/index.html

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.http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569In 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...

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