This chapter presents the proof process used by Thales and Autonomous Operator of Parisian Transports (RATP) to demonstrate the safety of the signaling systems used for the RATP network in Paris. It introduces the rail application concerned by the author's proof activities, the Thales system used for the metro. The chapter then presents the models used in the formal proof process, before describing the proof suite designed by Prover Technology. The results of application of the proof process to the Thales signaling system for RATP line are described and discussed in detail, before considering a number of potential improvements. The chapter presents a brief overview of the architecture of the PMI system. It discusses the computerized interlocking module (CIM) subsystem, which constitutes the operational core of the signaling system.
Safety Demonstration for a Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof
20.06.2014
43 pages
Aufsatz/Kapitel (Buch)
Elektronische Ressource
Englisch
Modeling Spacecraft Modes for Nominal and Off-nominal Operations
British Library Conference Proceedings | 2011
|IMPLEMENTING DEGRADED PERFORMANCE MODES IN AN AUTONOMOUS VEHICLE
Europäisches Patentamt | 2023
|