The Community for Technology Leaders
RSS Icon
Subscribe
Los Angeles, CA
March 31, 2009 to April 2, 2009
ISBN: 978-0-7695-3507-4
pp: 49-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.
INDEX TERMS
CTCS, RBC, Time Automata, Safety, BoundedLiveness, UPPAAL
CITATION
Jidong Lv, "Formal Modeling and Analysis of RBC Subsystem in CTCS Level 3 Using UPPAAL", CSIE, 2009, 2009 WRI World Congress on Computer Science and Information Engineering, CSIE, 2009 WRI World Congress on Computer Science and Information Engineering, CSIE 2009, pp. 49-53, doi:10.1109/CSIE.2009.49
22 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool