-
摘要: 为了确保列车运行控制系统设计和开发的正确性, 比较了仿真、测试和形式化3种能够验证系统设计正确性的方式。根据列车运行控制系统对安全的苛求性, 提出了4个与系统安全相关的重要特性, 即实时性、混成性、分布(并发)性、反应性, 并分析了与这些特性相关的具体形式化方法。通过对每种形式化方法的数学基础和应用范围的分析和归类, 给出了各种方法的优势和不足。分析结果表明: 任何形式化方法的应用都具有一定的局限性, 这是由模型检验和定理证明的本质所决定的; 指出了新方法提出、既有方法拓展以及多方法集成将是列车运行控制系统的形式化领域的方向。Abstract: To ensure the correctness of train control system design and development, the ways of simulation, test and formalization were compared. According to the safe critical attribute of train control system, the characters related to system safety were propounded such as real time, hybrid, distribution(concurrence) and reactivity, and the specific formal methods associated with every character were introduced in details. The analysis and classification of the methods were done based on their mathematical basis and applications, and their advantages and disadvantages were given.Analysis result indicates that every method has determinate limitations, which is determined by the essences of model checking and theory proving. It is pointed out that the presentation of new method, the expansion of existing methods and the integration of many methods will be the development trend of formalization in train control system.
-
表 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.htmLI 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)
计量
- 文章访问数: 718
- HTML全文浏览量: 78
- PDF下载量: 629
- 被引次数: 0
