During the last five years, Event-B formal modelling has been successfully applied to various railway systems to demonstrate safety early in the design process or once systems are in operation. This approach is aimed at formalising a safety reasoning instead of modelling every bit of the system. This approach is intrinsically fit to scale up to large systems (or system of systems), hence able to handle centralised or distributed systems.

This paper describes a formal analysis method applied at the software design level. The objective is to prove that a software specification and its implementation satisfy the expected system properties. In our case the analysed design is that of the Zone Controller of a CBTC developed using B. The B-Method is used to ensure that the implementation is correct wrt the software specification, but it does not guarantee that the algorithms described in the specification are correct wrt the system level requirements. Our analysis overcomes this shortcoming, providing a stronger assurance that the designed software meets its objectives. In particular, we prove that the implemented algorithms ensure that the track portion actually occupied by a train is covered by a protection envelope on the software side. The analysis is formalised with an Event-B model that is subject to tool-based inspections: animation with ProB and formal proof with Atelier B. In contrast to the existing B-Method model, our Event-B model links environment variables (the real position of the trains) with software variables (protection envelopes) and models the assumptions about the possible evolution of the environment. This analysis was carried out on an industrial scale software, consisting of 12000 lines of executable code, with immediate concrete results. This paper shows that, in addition to demonstrating compliance, this approach is clearly of interest from an industrial point of view.

Software in industrial products, such as in the railway industry, constantly evolves to meet new or changing requirements. For projects with a lifetime spanning decades (such as the control software for energy plants, for railway lines, etc.), keeping track of the original design rationale through time is a significant challenge.

This paper describes a safety analysis effort on RATP's communication-based train control (CBTC) system Octys. This CBTC is designed for multi-sourcing and brownfield deployment on an existing interlocking infrastructure. Octys is already in operation on several metro lines in Paris, and RATP plans its deployment on several other lines in the forthcoming years. Besides the size and complexity of the system, the main technical challenges of the analysis are to handle the existing interlocking functionalities without interfering with its design and to clearly identify the responsibilities of each subsystem supplier. The distinguishing aspect of this analysis is the emphasis put on intellectual rigor, this rigor being achieved by using formal proofs to structure arguments, then using the Atelier B tool to mechanically verify such proofs, encoded in the Event-B notation. With this approach, we obtain a rigorous mathematical proof of the safety at system level-a level that is usually covered by informal reasoning and domain expert knowledge only. Such proof is thus feasible and it brings to light and precisely records the knowledge and know-how of the domain experts that have designed the system.