Participation was free and we have got a lot of croissants.... and café.... and orange juice.

Road systems (Road systems: including ordinary traffic monitoring and street signal control systems and toll way (peage) systems with toll gate tickets an= d payment), railway systems (Railway systems: incl. mixed train traffic on general nets with, for example switch [aiguillage] interlocking and other signaling subsystems), air traffic systems (Air traffic systems: across ground control, terminal or tower control, area control, etc.), and, for example, container vessel shipping (Container line industry: across sea lane between harbours), all share underlying abstractions such as transportation nets with hubs (road intersections, train stations, airports and harbours) and links (road segments, train tracks, air and sea lanes) and their states of being open or closed for certain flows of traffic across hubs and along links, etc. In this talk we shall first hint at an abstract formal model for such transportation and then show how it can be refined into models for road traffic, train traffic and air traffic. Then we likewise hint at how such, so-called domain models --- which reflect only what there is "out there", in reality, before computing and communication --- can be rigorously transformed into requirements for respective traffic monitoring and control systems. The talk concludes with a discussion of issues of development of the right systems, that is, the systems that customers (that is, transportation and traffic authorities) expect to receive, and of systems which are right, that is, are correct.

La plateforme Rodin propose une série d'outils et de "plug_ins" liés, entre autres, au formalisme de Event-B (raffinement et preuves). Une exposé/démonstration de cette plateforme est présenté à l'aide d'exemples. Les étudinats d'ESIAL 3A Logiciels Embarqués sont venus suivre cet exposé et ont eu une présentation des techniques de preuve que l'on peut utiliser dans RODIN.

The development of structured programs is carried out either using bottom-up techniques, or top-down techniques; we show how refinement and proof can be used to help in the top-down development of structured imperative programs. When a problem is stated, the incremental proof-based methodology of event B starts by stating a very abstract model and further refinements lead to finer-grain event-based models which are used to build an algorithm. In this work, the main idea is to consider each procedure call as an abstract event of a model corresponding to the development of the procedure; generally, a procedure is specified by a pre/post specification and then the refinement process can lead to a set of events, which are then combined to obtain the body of the procedure. It means that the abstraction corresponds to the procedure call and the body is derived by the refinement process. The refinement process may also use recursive procedures and it supports the top-down refinement. The technique is illustrated by the sorting problem. Joint work with Dominique Méry

In many countries around the world, there is a crisis in the teaching of mathematics and computer science. Governments have tried to address the problem by investing in computers in schools; when they should have invested in teaching computer science in schools. Formal methods bridge the boundary between computing and mathematics in a natural way. Through my experience of teaching algorithmic thinking in schools, I have observed young children using concepts such as refinement, proof, abstraction, complexity, non-determinism, equivalence, etc... in their own reasoning about problems. I will argue that this ability needs to be better leveraged in order to improve both the teaching of mathematics but also to improve childrens' understanding of computer science as a discipline in its own right. I will give some concrete examples of the type of formal methods teaching that can be successful; and which has been motivated by the highly successful "computer science unplugged" educational research programme.