Formal Modeling and Analysis of RBC Subsystem in CTCS Level 3 Using UPPAAL

Author

Lv, Jidong ; Tang, Tao

Author_Institution

Traffic Control & Safety State Key Lab., Beijing Jiaotong Univ., Beijing, China

Volume

2

fYear

2009

fDate

March 31 2009-April 2 2009

Firstpage

49

Lastpage

53

Abstract

This paper analyses the function and performance of the software of RBC (Radio Block Center) subsystem in CTCS (Chinese Train Control System) level 3. It describes the formalization of RBC subsystem based on the theory of Timed automata. EQRS timed automata network model is built and based on the simulation and analysis of RBC subsystem, the safety and BoundedLiveness of RBC is validated using UPPAAL validation tool.

Keywords

automata theory; formal specification; formal verification; rail traffic; railway communication; railway engineering; CTCS level 3; Chinese train control system; Radio Block Center subsystem software; UPPAAL validation tool; formal analysis; formal modeling; timed automata theory; Analytical models; Automata; Communication system control; Information analysis; Performance analysis; Rail transportation; Railway safety; Real time systems; Software performance; Software safety; BoundedLiveness; CTCS; RBC; Safety; Time Automata; UPPAAL;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Science and Information Engineering, 2009 WRI World Congress on

Conference_Location

Los Angeles, CA

Print_ISBN

978-0-7695-3507-4

Type

conf

DOI

10.1109/CSIE.2009.49

Filename

5171299