Safety Demonstration for a Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof

Jean Marc Mota; Evguenia Dmitrieva; Amel Mammar; Paul Caspi; Salimeh Behnia; Nicolas Breton; Pascal Raymond

doi:10.1002/9781119004707.ch4

Safety Demonstration for a Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof

Jean Marc Mota, Evguenia Dmitrieva, Amel Mammar, Paul Caspi, Salimeh Behnia, Nicolas Breton, Pascal Raymond

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

Abstract

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.

Original language	English
Title of host publication	Formal Methods Applied to Industrial Complex Systems
Publisher	Wiley-Blackwell
Pages	71-113
Number of pages	43
Volume	9781848216327
ISBN (Electronic)	9781119004707
ISBN (Print)	9781848216327
DOIs	https://doi.org/10.1002/9781119004707.ch4
Publication status	Published - 29 Sept 2014

Keywords

Autonomous Operator of Parisian Transports (RATP)
Computerized interlocking module (CIM)
Formal proof process
PMI system
Prover Technology
Rail signaling systems
Safety demonstration
Thales

Access to Document

10.1002/9781119004707.ch4

Cite this

@inbook{74250b10f5b24d4aba90ee4c03849170,

title = "Safety Demonstration for a Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof",

abstract = "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.",

keywords = "Autonomous Operator of Parisian Transports (RATP), Computerized interlocking module (CIM), Formal proof process, PMI system, Prover Technology, Rail signaling systems, Safety demonstration, Thales",

author = "Mota, \{Jean Marc\} and Evguenia Dmitrieva and Amel Mammar and Paul Caspi and Salimeh Behnia and Nicolas Breton and Pascal Raymond",

note = "Publisher Copyright: {\textcopyright} 2014 John Wiley \& Sons, Inc.",

year = "2014",

month = sep,

day = "29",

doi = "10.1002/9781119004707.ch4",

language = "English",

isbn = "9781848216327",

volume = "9781848216327",

pages = "71--113",

booktitle = "Formal Methods Applied to Industrial Complex Systems",

publisher = "Wiley-Blackwell",

}

TY - CHAP

T1 - Safety Demonstration for a Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof

AU - Mota, Jean Marc

AU - Dmitrieva, Evguenia

AU - Mammar, Amel

AU - Caspi, Paul

AU - Behnia, Salimeh

AU - Breton, Nicolas

AU - Raymond, Pascal

PY - 2014/9/29

Y1 - 2014/9/29

N2 - 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.

AB - 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.

KW - Autonomous Operator of Parisian Transports (RATP)

KW - Computerized interlocking module (CIM)

KW - Formal proof process

KW - PMI system

KW - Prover Technology

KW - Rail signaling systems

KW - Safety demonstration

KW - Thales

U2 - 10.1002/9781119004707.ch4

DO - 10.1002/9781119004707.ch4

M3 - Chapter

AN - SCOPUS:84926405373

SN - 9781848216327

VL - 9781848216327

SP - 71

EP - 113

BT - Formal Methods Applied to Industrial Complex Systems

PB - Wiley-Blackwell

ER -

Safety Demonstration for a Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof

Abstract

Keywords

Access to Document

Fingerprint

Cite this