【作者】 张岩；

【导师】 唐涛；

【作者基本信息】 北京交通大学 ， 交通信息工程及控制， 2012， 博士

【摘要】 在列车运行控制系统中,软件负责与硬件共同实现核心功能,对于保障列车安全高效运营具有重要作用。软件故障是导致事故发生并造成生命财产损失的重要因素,所以研究针对软件内部故障和外部故障容忍的测试序列生成方法具有重要意义。列控系统软件具有并发性、反应式特性和行为空间庞大的特点,研究适合描述软件异常行为的建模方法和故障相关测试序列生成方法,已经成为列控系统软件的系统级黑盒安全性测试理论的研究重点。根据列控系统软件的特点及其故障相关测试需求,提出了专用的形式化建模及测试序列生成方法。建模方面,提出了一种进程模型的形式化定义及其图形化描述方法(Process Describe Method based on Colored Petri Net, ProcCPN)和描述基于异步通信机制的并发软件异常行为模型的分层建模方法。该方法具有以下特点：(1)基于严格的形式化定义；(2)包含使得大规模软件系统模型结构清晰的分层建模方法；(3)可以抽象地描述进程之间的通信参数,从而解决参数相关性约束问题；(4)继承了CPN的图形化优点。提出基于被测系统(System Under Test, SUT)弱互连性和系统弱互连性的静态死锁避免方法,证明了满足弱互连性是系统不存在死锁的必要条件,而非充分条件。提出了综合利用激发图(Ocurrence Graph, OG)、强连通图(Strongly Connected Component Graph, SCCG)、死标识和状态空间中的强连通分量来分析软件系统模型中死锁和活锁的方法,从而确保模型本身以及基于模型生成的测试序列的正确性。测试序列生成方面,提出了从软件的OG中提取SUT的输入输出标号迁移系统(Input-Output Labeled Transition System, IOLTS)语义的方法,从而可以在CPN Tools工具生成的OG上直接应用基于IOLTS语义的测试序列生成方法,解决了并发系统测试方法遇到的不可达状态过多的问题。并且以计算树逻辑(Computation Tree Logic, CTL)的扩展形式ASK-CTL为基础,通过定义ASK-CTL的反例、证例、故障相关测试目的(Fault Related Test Purpose, FRTP)公式和FRTP公式证明图等概念,提出FRTP公式证例路径的概念,扩充了传统基于反例路径的测试理论。对传统揭示(Reveal)关系概念进行扩展,基于故障相关观测目标(Fault Related Observation Objective, FROO)定义故障相关揭示关系(Fault Related Reveal Relation, FRRR),给出故障相关测试序列(Fault Related Test Sequence, FRTS)的形式化定义,证明了FRTS集是健全的和e完备的,从而规范了测试序列生成过程。给出了FRTP公式证例路径、FROO和FRTS生成算法,并将这些算法集成到CPN Tools工具上,实现了FRTS形式化自动生成工具。最后以中国列车运行控制系统3级(China Train Control System Level3, CTCS-3)车载设备软件为应用对象,进行软件系统建模、测试生成和测试执行的实例研究。结果说明,该方法可有效的描述异步通信机制下并发软件的异常行为,一定程度上解决了状态空间爆炸问题,且生成的针对软件故障的测试序列具有接近100%的软件故障检测率。给定一个期望测试的异常情况下故障容忍行为,本方法还可生成针对该行为的异常环境软件故障注入测试(Software Fault Injection Test, SFIT)的测试序列。更多还原

【Abstract】 ABSTRACT:The software, in the train control system is responsible to implement the key function together with the hardware, thus playing an important part in ensuring the high efficiency and safety of the train operation. The software fault is an important factor in causing an accident, which might cause the social life and property lose. So the research of the software internal fault and external fault tolerance oriented test sequence generating method is significant. The software in train control system has the features of concurrency, reactive and vast behavior space. The research of system-test level black box safety test theory for the software in the train control system should focus on the software exception behavior description oriented modeling method, and the fault related formal test sequence generation method.A dedicated formal modeling method and a test sequence generation method are proposed according to the features and the fault related test requirements of the software in train control system.To the modeling method, a formal definition of the process model and its graphical describing method named Process Describe Method based on Colored Petri Net (ProcCPN) is proposed, a hierarchy modeling method for describing the model of the asynchronous communication based exception behaviors of the concurrent software is then carried out. The characteristics of this method include:(1) It is based on the strict formal definition.(2) It includes hierarchy modeling method, which makes the structure of large-scale software system models clearer.(3) It can describe the communication parameters between processes in an abstract way, and solve the problem of constraint correlation of parameters.(4) It inherited the CPN’s merit of graphical description. The System Under Test (SUT) and system weak interoperability based deadlocks statically avoiding method is proposed. It is proved that the satisfaction of weak interoperability is a necessary condition to avoid deadlocks, and not a sufficient condition. The deadlock and livelock analyzing method for software system model is proposed using the Occurrence Graph (OG), the Strongly Connected Component Graph (SCCG), the dead markings and the strongly connected component of the state space. This method can ensure the accuracy of the model and the generated test sequence.To the test sequence generating method, the method of getting the IOLTS semantics of the SUT from the OG of the software is presented. Then the IOLTS semantics based test sequence generation method can be applied directly on the OG given by the CPN Tools. The problem of an excessive number of unreachable states is solved. ASK-CTL is an extension of the Computation Tree Logic (CTL). The definition of witness path for Fault Related Test Purpose (FRTP) formula is proposed based on the ASK-CTL oriented definition of the counterexamples, the witnesses, the formula of FRTP and the evident graph of the FRTP formula. Then the traditional testing theory which uses the counterexamples is extended. The Fault Related Reveal Relation (FRRR) is defined based on the formal definition of Fault Related Observation Objective (FROO) and the extension of the traditional definition of the reveal relation. Then the formal definition of the Fault Related Test Sequence (FRTS) suite is carried out and also proved to be sound and e complete. It promotes the standardization of test sequence generation process. The generation algorithms of the witness paths for FRTP formula, the FROO and the FRTS are proposed and integrated into the CPN Tools. Then the automatic FRTS generation formal method is realized.The presented software system modeling, test sequence generating and test execution methods are applied on the on-board equipment software of China Train Control System Level3(CTCS-3). The results show that these methods can describe the asynchronous communication based exception behaviors of concurrent software and avoid the rapid increase of state space. The generated test sequences for the testing of software faults can test out nearly100%faults in system software. Given a fault tolerance behavior in exception situation, these methods can also generate an exception environment test sequence of Software Fault Injection Test (SFIT) for this behavior.更多还原