基于HCSP的列控系统安全性建模与验证分析

吕继东; 唐涛; 李开成; 王海峰

基于HCSP的列控系统安全性建模与验证分析

北京交通大学轨道交通运行控制系统国家工程研究中心,北京 100044

基金项目: 国家自然科学基金资助项目（61304185）；中国铁路总公司科技研究开发计划课题（2014X003-D）。

详细信息

作者简介:
吕继东，讲师；唐涛，教授。

中图分类号: U284.482:U238:TP39
出版历程
- 收稿日期: 2016-06-07
- 刊出日期: 2017-01-25

Modeling and verification analysis for safety property of HCSP based train control system

National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China

摘要

摘要: 高速铁路列车运行控制系统是保证列车安全、高效运行的核心设备，如何验证系统功能的正确性从而提高系统的安全性是至关重要的。引入了一种基于进程演算的方法—混合通信顺序进程（HCSP ，Hybrid Communication Sequential Process），利用该方法对列控系统进行了形式化描述，并针对典型的场景—注册与启动场景进行了HCSP建模，通过引入转换规则，进行了相应模型转换，应用模型检验工具UPPAAL进行了仿真和功能验证，验证结论表明了场景模型功能的正确性以及方法的可行性。
- 列车运行控制系统 /
- 安全性 /
- 混合通信顺序进程 /
- 注册与启动 /
- 模型转换 /
- 验证
Abstract: The high speed train control system is a core equipment, which plays an important role in assuring safety and improving efficiency in railway. How to verify the correctness of the functions of system in order to improve the safety is especially important. In this article, the process calculus based method called hybrid communication sequential process(HCSP) was introduced. The formal description to the train control system was taken by HCSP. For typical scenarios, the scenarios of registration and start up were modeled by HCSP. By introducing transition rules, the corresponding model transformation was carried out. The model checking tool UPPAAL was used to simulate and verify the function. The results showed that the model was correct and the method was feasible.
- train control system /
- safety /
- hybrid communication sequential process(HCSP) /
- registration and start up /
- model transition /
- verification

HTML全文

参考文献(16)

[1]	季学胜，唐涛. CTCS-3 级列车运行控制系统综合测试平台研究[J]. 铁道通信信号，2007，43（7）：1-3. XUsheng Ji, Tang Tao . Research on CTCS level 3 train control system’ synthesis tests platform[J]. RAILWAY SIGNAI.LING & COMMUUICATION, 2007, 43（7）: 1-3.
[2]	古天龙. 软件开发的形式化方法[M]. 北京：高等教育出版社，2005. Tianlong Gu, Formal Methods of Software Development[M].Beijing: Higher Education Press, 2005.
[3]	Haxthausen A.E, Peleska J. Formal Development and Verification of a Distributed Railway Control System[J]. IEEE Transactions On Software Engineering, 2000, 26(8): 687-701.
[4]	Kirsten Berkenkotter Stefan Bisanz Ulrich Hannemann Jan Peleska. The HybridUML profile for UML 2.0[J]. International Journal on Software Tools for Technology, 2006, 8(2): 167–176.
[5]	Kirsten Berkenkotter, Stefan Bisanz, Ulrich Hannemann, JanPeleska. HybridUML profile for UML2.0. SVERTS Workshop at the UML 2003 Conference, October 2003[EB/OL].[2003-10-20]. http://www.verimag. imag.fr/EVENTS/2003/SVERTS/.
[6]	Paul Ziemann and Martin Gogolla. Validating OCL specifications with the USE tool - an example based on the BART case study[J]. In Thomas Arts and Wan Fokkink, editors, Proc. 8th Int. Workshop Formal Methods for Industrial Critical Systems (FMICS’2003), volume 80 of ENTCS. Elsevier, 2003.
[7]	R. Meyer, J. Faber, and A. Rybalchenko. Model checking duration Calculus: a practical approach[J]. In: K. Barkaoui,A. Cavalcanti, and A. Cerone (Eds.),Proc. Int’l Coll. on Theoret. Aspects of Computing (ICTAC),vol. 4281 of Lecture Notes in Computer Science, pp. 332-346.Springer, 2006.
[8]	Andre Platzer. Differential Dynamic Logic for Verifying Parametric Hybrid Systems[M]. Automated Reasoning with Analytic Tableaux and Related Methods, Springer Berlin / Heidelberg 2007, pp. 216-232.
[9]	Andre Platzer, Jan-David Quesel. European Train Control System: A Case Study in Formal Verification [M]. Lecture Notes in Computer Science, Springer Berlin 2009, pp. 246-265.
[10]	Jansen L,Meyer H M,Schnieder E. Technical Issues in Modelling the European Train Control Systems（ETCS） Using Coloured Petri Nets and Design/CPN Tools[R]. Aarhus Universitet. Workshop on Practical Use of Coloured Petri Nets and Design, Aarhus, 1998: 103-115.
[11]	Michael Meyer zu Horste and Eckehard Schnieder. Modeling train control systems with Petri nets-A functional referencearchitecture[C]. 2000 IEEE International Conference on System,man and Cybernetics. Nashville, TN , USA, 2000:3081-3086.
[12]	Zhou Chaochen,WangJi and Anders P.Ravn A Formal Description of Hybrid Systems[C]. in the Proc of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control Springer-Verlag New York, Inc. Secaucus, NJ, USA ,1996.
[13]	吕继东，唐涛. 高速铁路列控系统运营场景实时性的建模与验证[J]. 铁道学报，2011， 33（6）：54-61. Lu Ji-dong, TANG Tao. Modeling and Verification of Time Constraints of Operation Scenarions of Hign-speed Train Control System[J]. Journal of the China Railway Society, 2011, 33(6): 54-61
[14]	张曙光.CTCS-3 级列控系统总体技术方案[M]. 北京：中国铁道出版社，2008. Shuguang Zhang. The general technical Programme of CTCS 3 level train control system in railways for passengers [M]. Beijing: China Railway Publishing House, 2008.
[15]	Behrmann. G, Larsen. K.G, Moller. O, Divid..A, Pettersson. P and Wang Yi, UPPAAL - present and future[C]. In the Proc of the 40th IEEE Conference on Decision and Control Orlando, Florida USA, December 2001, pp. 2881-2886.
[16]	吕继东，唐涛，贾昊. 客运专线CTCS-3 级列控系统无线闭塞中心的建模与验证[J]. 铁道学报，2010，32（6）：34-42. Lu Jidong, TANG Tao, JIA Hao. Modeling and Verification of Radio Block Center of CTCS-3 Train Control System for Dedicated Passengers Lines[J]. Journal of the China Railway Society, 2010, 32(6): 34-42.