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.
展开▼
