详情

原文传递列车运行控制系统软件故障相关形式化测试方法

论文题名：	列车运行控制系统软件故障相关形式化测试方法
关键词：	列车运行控制系统;安全软件;测试序列生成方法;故障容忍行为
摘要：	在列车运行控制系统中，软件负责与硬件共同实现核心功能，对于保障列车安全高效运营具有重要作用。软件故障是导致事故发生并造成生命财产损失的重要因素，所以研究针对软件内部故障和外部故障容忍的测试序列生成方法具有重要意义。列控系统软件具有并发性、反应式特性和行为空间庞大的特点，研究适合描述软件异常行为的建模方法和故障相关测试序列生成方法，已经成为列控系统软件的系统级黑盒安全性测试理论的研究重点。　　根据列控系统软件的特点及其故障相关测试需求，提出了专用的形式化建模及测试序列生成方法。　　建模方面，提出了一种进程模型的形式化定义及其图形化描述方法(ProcessDescribe Method based on Colored Petri Net，ProcCPN)和描述基于异步通信机制的并发软件异常行为模型的分层建模方法。该方法具有以下特点：(1)基于严格的形式化定义；(2)包含使得大规模软件系统模型结构清晰的分层建模方法；(3)可以抽象地描述进程之间的通信参数，从而解决参数相关性约束问题；(4)继承了CPN的图形化优点。提出基于被测系统(System Under Test，SUT)弱互连性和系统弱互连性的静态死锁避免方法，证明了满足弱互连性是系统不存在死锁的必要条件，而非充分条件。提出了综合利用激发图(Ocurrence Graph，OG)、强连通图(StronglyConnected Component Graph，SCCG)、死标识和状态空间中的强连通分量来分析软件系统模型中死锁和活锁的方法，从而确保模型本身以及基于模型生成的测试序列的正确性。　　测试序列生成方面，提出了从软件的OG中提取SUT的输入输出标号迁移系统(Input-Output Labeled Transition System，IOLTS)语义的方法，从而可以在CPNTools工具生成的OG上直接应用基于IOLTS语义的测试序列生成方法，解决了并发系统测试方法遇到的不可达状态过多的问题。并且以计算树逻辑(ComputationTree Logic，CTL)的扩展形式ASK-CTL为基础，通过定义ASK-CTL的反例、证例、故障相关测试目的(Fault Related Test Purpose，FRTP)公式和FRTP公式证明图等概念，提出FRTP公式证例路径的概念，扩充了传统基于反例路径的测试理论。对传统揭示(Reveal)关系概念进行扩展，基于故障相关观测目标(Fault RelatedObservation 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)的测试序列。
作者：	张岩
专业：	交通信息工程及控制
导师：	唐涛
授予学位：	博士
授予学位单位：	北京交通大学
学位年度：	2012
正文语种：	中文