This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 WRI World Congress on Computer Science and Information Engineering
Formal Modeling and Analysis of RBC Subsystem in CTCS Level 3 Using UPPAAL
Los Angeles, California USA
March 31-April 02
ISBN: 978-0-7695-3507-4
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, Tao Tang, "Formal Modeling and Analysis of RBC Subsystem in CTCS Level 3 Using UPPAAL," csie, vol. 2, pp.49-53, 2009 WRI World Congress on Computer Science and Information Engineering, 2009
Usage of this product signifies your acceptance of the Terms of Use.