This paper presents the formal development of the memory management module of a real time operating system. The interesting feature of this type of memory manager is that its dynamic memory allocation/reallocation mechanism behaves in O(1) (no loops). This brings a serious challenge on the "correct by construction" approach used to build this kind of system. This is due to the necessity to elaborate some delicate algorithms associated with complex data structures. To overcome this challenge, we follow the refinement principles of Event-B: we construct the proved executable code from some initial requirements. This development is interesting because some of the encountered problems are rather necessary to be studied in formal proved developments, among which are a modular encapsulation development, the design pattern of a linked list, and the usage of guarded events to develop pre-conditioned operations. It also gives us the opportunity to study a complex program construction in some general terms going beyond this specific example.

Event-B has given developers the opportunity to construct models of complex systems which are correct by construction. However, there is no systematic approach, especially in terms of reusing, which could help with the construction of these models. We introduce the notion of design patterns within the framework of Event-B to shorten this gap. Our approach preserves the correctness of the models which is critical in formal methods and also reduces the proving effort. Within our approach, an Event-B design pattern is just another model devoted to the formalisation of a typical sub-problem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a larger model. We also present the interaction between developers and the future tool support within the associated Rodin Platform of Event-B. The approach has been applied successfully in some medium-size industrial case studies.

This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

Two real projects using the B formal method are quickly presented. They show how some important parts of complex systems can be developed in such a way that the outcome is "correct by construction". A number of factors are then analyzed relating the pros, the cons, and the difficulties in applying this approach in Industry.

Abstract. The IEEE 1394 tree identify protocol illustrates the adequacy of the event-driven approach used together with the B Method. This approach provides a complete framework for developing mathematical models of distributed algorithms. A specific development is made of a series of more and more refined models. Each model is made of a number of static properties (the invariant) and dynamic parts (the guarded events). The internal consistency of each model as well as its correctness with regard to its previous abstraction are proved with the proof engine of Atelier B, which is the tool associated with B. In the case of IEEE 1394 tree identify protocol, the initial model is very primitive: it provides the basic properties of the graph (symmetry, acyclicity, connectivity), and its dynamic parts essentially contain a single event which elects the leader in one shot. Further refinements introduce more events, showing how each node of the graph non-deterministically participates in the leader election. At some stage in the development, message passing is introduced. This raises a specific potential contention problem, whose solution is given. The last stage of the refinement completely localises the events by making them take decisions based on local data only.