留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

形式化方法在列车运行控制系统中的应用

曹源 唐涛 徐田华 穆建成

曹源, 唐涛, 徐田华, 穆建成. 形式化方法在列车运行控制系统中的应用[J]. 交通运输工程学报, 2010, 10(1): 112-126. doi: 10.19818/j.cnki.1671-1637.2010.01.020
引用本文: 曹源, 唐涛, 徐田华, 穆建成. 形式化方法在列车运行控制系统中的应用[J]. 交通运输工程学报, 2010, 10(1): 112-126. doi: 10.19818/j.cnki.1671-1637.2010.01.020
CAO Yuan, TANG Tao, XU Tian-hua, MU Jian-cheng. Application of formal methods in train control system[J]. Journal of Traffic and Transportation Engineering, 2010, 10(1): 112-126. doi: 10.19818/j.cnki.1671-1637.2010.01.020
Citation: CAO Yuan, TANG Tao, XU Tian-hua, MU Jian-cheng. Application of formal methods in train control system[J]. Journal of Traffic and Transportation Engineering, 2010, 10(1): 112-126. doi: 10.19818/j.cnki.1671-1637.2010.01.020

形式化方法在列车运行控制系统中的应用

doi: 10.19818/j.cnki.1671-1637.2010.01.020
基金项目: 

国家自然科学基金项目 60634010

国家自然科学基金项目 60736047

“十一五”国家科技支撑计划项目 2006BAG02B04

轨道交通控制与安全国家重点实验室自主研究课题 RCS2008ZZ005

高等学校博士学科点专项科研基金项目 20070004005

详细信息
    作者简介:

    曹源(1982-), 男, 河南开封人, 北京交通大学工学博士研究生, 从事列车运行控制系统的形式化研究

    唐涛(1963-), 男, 河南洛阳人, 北京交通大学教授

  • 中图分类号: U283.2

Application of formal methods in train control system

More Information
  • 摘要: 为了确保列车运行控制系统设计和开发的正确性, 比较了仿真、测试和形式化3种能够验证系统设计正确性的方式。根据列车运行控制系统对安全的苛求性, 提出了4个与系统安全相关的重要特性, 即实时性、混成性、分布(并发)性、反应性, 并分析了与这些特性相关的具体形式化方法。通过对每种形式化方法的数学基础和应用范围的分析和归类, 给出了各种方法的优势和不足。分析结果表明: 任何形式化方法的应用都具有一定的局限性, 这是由模型检验和定理证明的本质所决定的; 指出了新方法提出、既有方法拓展以及多方法集成将是列车运行控制系统的形式化领域的方向。

     

  • 图  1  ETCS-2级信道模型

    Figure  1.  Channel model of ETCS-2

    图  2  ETCS-2级系统模型

    Figure  2.  System model of ETCS-2

    图  3  ETCS中一个实时性验证案例

    Figure  3.  A case of realtime verification in ETCS

    图  4  一个dTL验证超速防护的案例

    Figure  4.  A case of speed protection using dTL

    图  5  一个脚本层面的CPN模型

    Figure  5.  A scenario of CPN model

    图  6  激励序列

    Figure  6.  Stimuli sequence

    图  7  S3 Tool Chain流程

    Figure  7.  Flow of S3 tool chain

    图  8  简化故障树与Statemate的混合模型

    Figure  8.  Hybrid model of simplify fault tree and statemate

    图  9  列控系统中的分布式结构

    Figure  9.  Distributed structure of train control system

    图  10  BART线上的安全约束

    Figure  10.  Safety constraints in BART line

    表  1  形式化方法的比较

    Table  1.   Comparison of different formal methods

    方法 数学基础 描述特性 分布性 实时性 混成性 反应性
    Z/OZ 集合论、一阶逻辑 复杂系统结构以及功能、复杂数据结构与算法
    CSP 进程代数 并发事件、逻辑关系
    DC(限制子集) 区间逻辑、代数论(自动机理论) 连续时间、时序逻辑关系 √√
    CSP-OZ-DC(限制子集) 进程代数、集合论、数理逻辑、DC(自动机理论) 较复杂系统结构以及功能、较复杂数据结构与算法、连续时间
    RAISE 进程代数、集合论、一阶逻辑 复杂系统结构以及功能、数据结构与算法、并发事件 √√
    TRAISE 集合论、一阶逻辑、进程代数、DC 复杂系统结构以及功能、复杂数据结构与算法、并发事件、连续时间 √√
    Domain Langauge 代数理论、一阶逻辑 连续的重复动作、与时间相关的状态变化
    SPN 连续Markov链 随机和连续时间、简单结构以及功能 √√
    CPN 自动机理论 系统结构以及功能、较复杂规模系逻辑关系
    S3 Tool Chain 连续Markov链、交互式Markov链 较复杂的结构以及功能、较复杂的数据结构与算法、并发事件、随机和连续时间 √√
    dTL 一阶动态逻辑、微积分 逻辑关系、离散和连续的时间 √√
    注: “√”表示能够对此特性进行形式化; “√√”表示适合对此特性进行形式化。
    下载: 导出CSV
  • [1] CLARKE E M, GRUMBERG O, PELED D. Model Checking[M]. Cambridge: The MIT Press, 2000.
    [2] 燕飞. 轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D]. 北京: 北京交通大学, 2006.

    YAN Fei. The formal modelling and model checking research of rail transportation train control system[D]. Beijing: Beijing Jiaotong University, 2006. (in Chinese)
    [3] EN 50129: 2002, rail way applications-communication, signalling and processing systems-safety related electronic systems for signalling[S].
    [4] IEC 61508-1: 1997, functional safety of electrical/electronic/programmable electronic safety-related systems[S].
    [5] ZIMMERMANN A, HOMMEL G. A train control system case study in model-based real ti me system design[C]∥ IEEE. Proceedings of the 17th International Symposium on Parallel and Distributed Processing. Washington DC: IEEE, 2003: 118-126.
    [6] ZIMMERMANN A, HOMMEL G. Towards modeling and evaluation of ETCS real-time communication and operation[J]. The Journal of Systems and Software, 2005, 77(1): 47-54. doi: 10.1016/j.jss.2003.12.039
    [7] MEYER R. Model-checking von phasen-event-automaten bezüglich duration calculus formeln mittels testautomaten[D]. Oldenburg: Universitat Oldenburg, 2005.
    [8] Subset-052, radio transmission FFFIS for Euroradio[S].
    [9] 李晓山, 周巢尘. 时段演算综述[J]. 计算机学报, 1994, 17(11): 842-851. https://www.cnki.com.cn/Article/CJFDTOTAL-JSJX411.005.htm

    LI Xaio-shan, ZHOU Chao-chen. Duration calculi: an overview[J]. Chinese Journal of Computers, 1994, 17(11): 842-851. (in Chinese) https://www.cnki.com.cn/Article/CJFDTOTAL-JSJX411.005.htm
    [10] ZHOU C C, HANSEN M R. Duration Calculus: a Formal Approach to Real-Time Systems[M]. Essex: Springer, 2004.
    [11] MEYER R, FABERJ, HOENICKEJ, et al. Model checking duration calculus: a practical approach[J]. Formal Aspects of Computing, 2008, 20(4/5): 481-505.
    [12] FABER J. Verifying real-ti me aspects of the European train control system[C]∥ University of Copenhagen. Proceedings of the 17th Nordic Workshop on Programming Theory. Copenhagen: DIKU, 2005: 67-70.
    [13] TAPKEN J. Model-checking of duration calculus specifications[D]. Oldenburg: Universitat Oldenburg, 2001.
    [14] DIERKS H, TAPKENJ. Moby/DC—a tool for model-checking parametric real-time specifications[J]. Tools and Algorithms for the Construction and Analysis of Systems, 2003, 2619: 271-277.
    [15] SCHAFER A. Combining real-time model-checking and fault tree analysis[C]∥ Institute of Science and Technology of Information. The 12th International Formal Methods Europe Symposium. Pisa: FME, 2003: 522-541.
    [16] PLATZER A. Differential dynamic logic for verifying parametric hybrid systems[J]. Automated Reasoning with Analytic Tableaux and Related Methods, 2007, 4548: 216-232.
    [17] PLATZER A. Atemporal dynamic logic for verifying hybrid system invariants[J]. Logical Foundations of Computer Science, 2007, 4514: 457-471.
    [18] PLATZER A, QUESEL J D. Logical verification and systematic parametric analysisintrain control[J]. Lecture Notes in Computer Science, 2008, 4981: 646-649.
    [19] ZU HORSTE M M. Modelling and si mulation of train control systems using petri nets[C]∥ Trier University. Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Toulouse: Springer, 1999: 1867-1883.
    [20] AVACS S3. Afault tree based model for ETCS application level 2[R]. Bonn: AVACS, 2007.
    [21] AVACS S3. Brake risk assessment for ETCStrain platoons[R]. Bonn: AVACS, 2007.
    [22] HERBSTRITT M, WI MMER R, PEIKENKAMP T, et al. Analysis of large safety-critical systems: a quantitative approach[R]. Bonn: AVACS, 2006.
    [23] BODE E, HERBSTRITT M, HERMANNS H, et al. Compositional performability evaluation for statemate[C]∥ IEEE. Third International Conference on the Quantitative Evaluation of Systems. California: IEEE, 2006: 167-178.
    [24] FABERJ, JACOBS S, VIORICAS S. Verifying CSP-OZ-DC specifications with complex data types and timing parameters[C]∥ University of Oxford. Integrated Formal Methods 2007. Oxford: University of Oxford, 2007: 233-252.
    [25] 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. doi: 10.1109/32.879808
    [26] HAXTHAUSEN A E, PELESKA J. A domain specific language for rail way control systems[C]∥ ENGELS G, SAUER S. Proceedings of the Sixth Biennial World Conference on Integrated Design and Process Technology. California: University of Paderborn, 2002: 1-7.
    [27] JANSENL, ZU HORSTE M M, SCHNIEDER E. Technical issues in modellingthe Europeantrain control system(ETCS) using coloured petri nets and design/CPNtools[C]∥Aarhus University. Workshop on Practical Use of Coloured Petri Nets and Design. Aarhus: Aarhus University, 1998: 103-115.
    [28] EINER S, SLOVAK R, SCHNIEDER E. Modeling train control systems with petri nets—an operational specification[C]∥IEEE. International Conference on Systems, Man, and Cybernetics. Nashville: IEEE, 2000: 3207-3211.
    [29] ZU HORSTE M M, SCHNIEDER E. Modeling train control systems with petri nets—a functional reference-architecture[C]∥IEEE. International Conference on Systems, Man, and Cybernetics. Nashville: IEEE, 2000: 3081-3086.
    [30] OLDEROG E R. Automatic verification of combined specifications: an overview[J]. Electronic Notes in Theoretical Computer Science, 2008(207): 3-16.
    [31] JOCHEN H, PATRICK M. Model-checking of specifications integrating processes, data and ti me[C]∥ FITZGERALD J, HAYESI J, TARLECKI A. International Symposium of Formal Methods Europe. Newcastle: Springer, 2005: 465-480.
    [32] JOCHEN H. Combination of processes, data, and time[D]. Oldenburg: Universitat Oldenburg, 2006.
    [33] BRÜCKNER I, WEHRHEI M H. Slicing an integrated formal method for verification[C]∥LAU K K, BANACH R. Seventh International Conference on Formal Engineering Methods. Manchester: Springer, 2005: 360-374.
    [34] BRÜCKNERI, WEHRHEI M H. Slicing object-z specifications for verification[C]∥ University of Surrey. 4th International Conference of B and Z Users. Guildford: Springer, 2005: 415-434.
    [35] GEORGE C, HAXTHAUSEN A E, HUGHES S, et al. The RAISE Development Method[M]. Hertfordshire: Prentice Hall Int, 1995.
    [36] HAXTHAUSEN A E, PELESKA J. A distributed railway control system selected proofs[R]. Kongens Lyngby: DTU, 2000.
    [37] MADSEN M S. Modelling a distributed rail way control system[D]. Kongens Lyngby: Technical University of Denmark, 2005.
    [38] XI A Y, CHRIS G. An operational semantics for timed raise[C]∥Trier University. Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Toulouse: Springer, 1999: 1008-1027.
    [39] LI Li, HE Ji-feng. A denotational semantics of timed RSL using duration calculus[J]. Journal of Software, 2001, 12(6): 802-815.
    [40] KAPUR D, WI NTER V L. On the construction of a domain language for a class of reactive systems[C]∥ WINTER V L, BHATTACHARYA S. The Kluwer International Series in Engineering and Computer Science. Boston: Kluwer Academic Publishing, 2001: 169-196.
    [41] WINTER V L, KAPUR D, BERG R S. A refinement-based approachto developing software controllers for train systems[C]∥ WINTER VL, BHATTACHARYAS. The Kluwer International Series in Engineering and Computer Science. Boston: Kluwer Academic Publishing, 2001: 197-240.
    [42] WINTER V L, KAPUR D, BERG R S. Formal specification and refinement of a safe train control function[C]∥ KORDON F, LEMOI NE M. Methods for Embedded Distributed Systems: How to Master the Complexity. Boston: Kluwer Academic Publishing, 2004: 25-64.
    [43] WINTER V L, KAPUR D. Towards dynamic partitioning of reactive systembehavior: a train controller case study[C]∥KORDON F, SZTIPANOVITSJ. Reliable Systems on Unreliable Networked Platforms. Berlin: Springer, 2007: 47-69.
    [44] VIORICA S S. Hierarchic reasoning in local theory extensions[C]∥ ROBERT N. International Conference on Automated Deduction. Tallinn: Springer, 2005: 219-234.
    [45] SWENJ, VIORICAS S. Applications of hierarchical reasoning in the verification of complex systems[J]. Electronic Notes in Theoretical Computer Science, 2007, 174(8): 39-54.
    [46] NAZIR A Z. Modeling and formal specification of automated train control system using z notation[C]∥ Mohammad Ali Jinnah University. Multitopic Conference IEEE. Islamabad: IEEE, 2006: 438-443.
  • 加载中
图(10) / 表(1)
计量
  • 文章访问数:  833
  • HTML全文浏览量:  87
  • PDF下载量:  641
  • 被引次数: 0
出版历程
  • 收稿日期:  2009-10-18
  • 刊出日期:  2010-02-25

目录

    /

    返回文章
    返回