Information Technology Reference
In-Depth Information
Formal Method and its Application on Train
Operation Control System of Chinese
high-speed Railway
Tao Tang
Beijing Jiaotong University
ttang@center.njtu.edu.cn
Abstract. With the development of the economic and society of
China, a high speed transport method is urgently required to solve
the travel problems of people. The train had been speeded up from
120 km/h to
250 km/h in the main line network. Chinese High Speed
railway has been rapidly developed. Railway plays a more and more
important role in the Chinese transportation systems. For the safety
and e ciency of high speed railway, Chinese Train Control system
(CTCS) is developed and some new technologies are reseached.
CTCS Level3 is the train control system used in Chinese High speed
railway. This system makes use of GSM-R to complete the safe com-
munication between onboard subsystem and RBC subsystem, and
employs the track circuit as a backup communicating approach to
ensure the safety of the system. Now in China, CTCS Level3 sys-
tem has already been used in four high speed railway lines, the total
length reached 2076 km . And the line from Beijing to Shanghai will
be put into operation next year, which also uses CTCS Level3.
Toguaranteethesafeoperationofthetrainandimprovethee ciency
of railway tra c, we make use of many formal methods and propose
some approaches of modeling, formal verification and developing of
the CTCS Level3 train control system, including the Specification
Validation and Verification, Hybrid system Modeling and Verifica-
tion, model based test sequence generation approach and SCADE
based safety critical system development method. The advantages of
our method are: Establish a track chain among the system specifica-
tion, model, model checking tools and verification results; generate
test sequences automatically and generate safety code automatically.
Search WWH ::




Custom Search