应用ETDFA生成CBTC联锁软件形式化模型的方法

Method for Generating CBTC Interlocking Software′s Formal System Model Using ETDFA

摘要:

CBTC系统的联锁软件为SIL4级的高安全、高可靠软件,目前广泛使用的软件测试和仿真验证的结果严重依赖选取的测试向量,要保证高覆盖率的测试十分困难;EN50128中强烈推荐SIL4等级的软件使用形式化方法完成软件需求规格说明书和软件设计,因此,采用形式化的方法设计软件,是构造高可靠、高安全软件的一个重要途径;总结了现有的CBTC系统中联锁子系统集成方式及优缺点,并使用事件确定有限自动机ETDFA(event deterministic finite automata)模型对适用性更优的升级型集成方式的联锁软件的联锁逻辑完成形式化定义,保证联锁逻辑的正确性,减少软件的不确定性描述;以办理进路为例生成联锁对象的ETDFA模型,验证该方法的有效性和可行性;该方法不仅为CBTC联锁软件的设计与开发提供新思路,而且有助于安全苛求软件的形式化验证与分析,提高联锁软件的安全性和正确性。

Abstract:

The safety and integrity level of Computer interlocking software in CBTC(communication based train control) system is SIL4, which is high security and high reliability software. The current widely used software testing and simulation results rely heavily on the selected test vector, to ensure high coverage of the test is very difficult. EN50128 strongly recommended SIL4 level of software using formal methods to complete the software requirements specification and software design, therefore, using formal methods to design software is an important way to build high reliability and high security software. This paper summarizes the existing integrated approaches and advantages and disadvantages of the interlocking subsystem in the CBTC system, and uses the ETDFA (event deterministic finite automata) model to realize the formal definition of upgrade type interlocking software, which ensures the correctness of the interlocking logic, and reduces the uncertainty description of the software. This paper takes creating route as an example to generate the ETDFA model of the interlocking object, and verifies the validity and feasibility of the method. This method not only provides new ideas for the design and development of CBTC interlocking software, but also contributes to the formal verification and analysis of security demanding software, and improves the security and correctness of interlocking software.