列车运行控制系统软件故障相关形式化测试方法
|
摘要
在列车运行控制系统中,软件负责与硬件共同实现核心功能,对于保障列车安全高效运营具有重要作用。软件故障是导致事故发生并造成生命财产损失的重要因素,所以研究针对软件内部故障和外部故障容忍的测试序列生成方法具有重要意义。列控系统软件具有并发性、反应式特性和行为空间庞大的特点,研究适合描述软件异常行为的建模方法和故障相关测试序列生成方法,已经成为列控系统软件的系统级黑盒安全性测试理论的研究重点。
根据列控系统软件的特点及其故障相关测试需求,提出了专用的形式化建模及测试序列生成方法。
建模方面,提出了一种进程模型的形式化定义及其图形化描述方法(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: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.
根据列控系统软件的特点及其故障相关测试需求,提出了专用的形式化建模及测试序列生成方法。
建模方面,提出了一种进程模型的形式化定义及其图形化描述方法(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: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.
引文
[1]Craigen D. Formal methods, EVES, and safety critical systems[R]. Ontario, Canada: Minister of National Defence,1994.
[2]Papadopoulos Y, Mcdermid. The potential for a generic approach to certification of safety critical systems in the transportation sector[J]. Reliability Engineering & System Safety, 1999,63(1):47-66.
[3]孟庆宇.尼崎事故的反思[J].铁道知识,2006,(4)：24-25.
[4]徐应诗,刘斌,阮镰.基于故障注入的仿真测试方法过程框架[J].测控技术,2007,26(10)：50-56.
[5]CENELEC. EN50128--2011. Railway application-communications, signaling and processing systems-software for railway control and protection systems[S]. UK:CENELEC, 2011.
[6]陈锦富,卢炎生,谢晓东.软件错误注入测试技术研究[J].软件学报,2009,20(6)：1425—1443.
[7]张岩,唐涛,燕飞.CBTC数据通信系统性能分析模型及应用研究[J].铁道学报,2011,33(5)：60-65.
[8]Zhang Y, Zhu L, Chen L, et al. A method for simulation and analysis of trackside data communication system in CBTC[C]. Proceedings of the 2009 International Conference on Communications and Mobile Computing Kunming:IEEE Computer Society,2009:529-533.
[9]宋沛东,张勇.CTCS3仿真测试平台一RBC仿真子系统的设计与实现[J].中国科技信息,2008,(1)：100—103.
[10]铁道部科技司CTCS-3级列控系统标准规范-CTCS-3级列控系统系统需求规范(SRS) [M].北京：中国铁道出版社,2009.
[11]Eliane M, Ana M A. ATIFS:a testing toolset with software fault injection[C]. Proceedings of the Conference of York Computer Science Yellow Report 2003, UK:Department of Computer Science at York,2003:1-3.
[12]Jonas B. Early fault detection with model-based testing[C]. Proceedings of the 7th ACM SIGPLAN workshop on ERLANG, Victoria, BC, Canada:ACM Press,2008:9-20.
[13]Hierons R, Bogdanov K, Bowen J, et al. Using formal specifications to support testing[J]. ACM Computing Surveys,2009,41(2):1-76.
[14]Offutt J, Liu S, Abdurazik A, et al. Generating test data from state-based specifications[J]. The Journal of Software Testing, Verification and Reliability,2003,13(1):25-53.
[15]吴芳美.铁路安全软件测试评估[M].北京：中国铁道出版社,2001.
[16]张岩,唐涛,马连川.基于交换式以太网安全通信协议的模型和仿真研究[J].铁道学报,2010,32(3)：43—48.
[17]Raymond P, Nicollin X, Halbwachs N, et al. Automatic testing of reactive systems[C]. Proceedings of the 19th IEEE Conference of Real-Time Systems Symposium, Madrid, Spain: IEEE Computer Society,1998:200-209.
[18]Grard B, Georges G. The ESTEREL synchronous programming language:design, semantics, implementation[J]. Science of Computer Programming,1992,19(2):87-152.
[19]Caspi P, Pilaud D, Halbwachs N, et al. LUSTRE:a declarative language for programming synchronous systems[C]. Proceedings of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, West Germany:ACM Press,1987:178-188.
[20]Le Guernic P, Benveniste A, Bournai P, et al. Signal-A data flow-oriented language for signal processing[J]. Acoustics, Speech and Signal Processing, IEEE Transactions on,1986,34(2): 362-374.
[21]Apirukvorapinit P. Search-based approach of automated test generation for state-based components[D]. Chicago, IL, USA:Illinois Institute of Technology,2005.
[22]燕飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D].北京：北京交通大学,2006.
[23]马均飞,郑文强.软件测试设计[M].北京：电子工业出版社,2011.
[24]徐中伟,吴芳美.形式化故障树分析建模和软件安全性测试[J].同济大学学报(自然科学版),2001,29(11)：1299—1302.
[25]Tommaso P D, Flammini F, Lazzaro A, et al. The simulation of anomalies in the functional testing of the ERTMS/ETCS trackside system[C]. Proceedings of the 9th IEEE International Symposium on High-Assurance Systems Engineering, Heidelberg, Germany:IEEE Computer Society,2005:131-139.
[26]喻钢,熊静,徐中伟.通用的安全苛求软件安全性测试方法[J].计算机工程,2010,36(17)：28-29.
[27]喻钢,徐中伟,杜军威.场景一事件驱动的安全苛求软件系统仿真测试脚本语言研究[J].计算机应用,2010,30(2)：374-379.
[28]章文婷,徐中伟,喻刚.面向安全苛求软件的测试用例自动生成[J].计算机应用研究,2009,26(1)：140—142+174.
[29]周绍君,徐中伟,喻钢.面向安全需求的测试用例自动生成技术研究[J].计算机工程与应用,2009,45(28)：75—78.
[30]ERTMS UNISIG SUBSET 076-2--2003. Methodology to prepare features, Version 2.2.2[S]. EU:ERTMS,2003.
[31]ERTMS UNISIG. SUBSET 076-3--2003 Methodology of testing, Version 2.2.2[S]. EU: ERTMS,2003.
[32]ERTMS UNISIG. SUBSET076-4-1--2003. Test sequence generation:methodology and rules, Version 2.2.2[S]. EU:ERTMS 2003.
[33]ERTMS UNISIG. SUBSET-094-0--2003. Functional requirements for an on board reference test facility,Version 1.0.0[S]. EU:ERTMS,2003.
[34]季学胜,李开成,张勇.CTCS-3级列控系统测试案例生成方法的研究[J].铁道通信信号,2009,45(10)：1—5.
[35]王春花.无线闭塞中心的测试方法研究[D].北京：北京交通大学,2008.
[36]De Nicola G, Di Tommaso.P, Esposito R, et al. A hybrid testing methodology for railway control systems[J]. Lecture Notes in Computer Science,2004,3219:116-129.
[37]Lee J D, Jung J I, Lee J H, et al. Verification and conformance test generation of communication protocol for railway signaling systems[J]. Computer Standards & Interfaces, 2007,29(2):143-151.
[38]Lee J H, Hwang J G, Shin D, et al. Development of verification and conformance testing tools for a railway signaling communication protocol[J]. Computer Standards & Interfaces, 2009,31(2):362-371.
[39]章慧,张勇.CTCS3级列控系统车载设备测试方法研究[J].铁路计算机应用,2008,17(4)：23-27.
[40]张勇,于超琦.CTCS-3级列控系统车载设备测试序列优化生成方法[J].中国铁道科学,2011,32(3)：100—106.
[41]赵显琼,唐涛.多端口形式化测试自动生成方法在CTCS-3车载系统中的应用[J].铁道学报,2011,33(7)：44-51.
[42]赵显琼,李开成,唐涛.基于TTCN-3的CTCS-3级列车运行控制系统自动测试方法[J].铁道通信信号,2010,46(7)：15-20.
[43]Angeletti D, Giunchiglia E, Narizzano M, et al. Using bounded model checking for coverage analysis of safety-critical software in an industrial setting[J]. Journal of Automated Reasoning,2010,45(4):397-414.
[44]李弋强,徐中伟,喻钢.面向安全需求的安全通信协议测试序列生成算法[J].计算机应用,2009,29(7)：1828-1831+1848.
[45]Tretmans J. Testing concurrent systems:a formal approach[C]. Proceedings of the 10th International Conference on Concurrency Theory, Eindhoven, Netherlands:Springer-Verlag, 1999:46-65.
[46]Medikonda B S, Panchumarthy S R. An approach to modeling software safety in safety-critical systems[J]. Journal of Computer Science,2009,5(4):311-322.
[47]Flammini F. Dependability assurance of real-time embedded control systems[M]. New York: Nova Science Publishers,2010.
[48]IEC. IEC 61508--1998. Functional safety of electrical/electronic/programmable electronic safety-related systems[S]. IEC,1998.
[49]Susannc K, Raimund K, Peter P. Development of a framework for automated systematic testing of safety-critical embedded systems[C]. Proceedings of the 2006 International Workshop on Intelligent Solutions in Embedded Systems, Vienna:IEEE Computer Society, 2006:1-13.
[50]Tracey N, Clark J, Mcdermid J, et al. Integrating safety analysis with automatic test-data generation for software safety verification[C]. Proceedings of the Conference of 17th International System Safety, Orlando, FL:System Safety Society,1999:128-137.
[51]Rayadurgam S. Automatic test-case generation from formal models of software[D]. Minnesota:University of Minnesota,2004.
[52]Rayadurgam S, Heimdahl M P E. Coverage based test-case generation using model checkers[C]. Proceedings of the 8th Annual IEEE International Conference on the Engineering of Computer Based Systems, Washington, DC, USA, USA:IEEE Computer Society,2001:83-91.
[53]Tracey N, Clark J, Mander K, et al. Automated test-data generation for exception conditions[J]. Software:Practice and Experience,2000,30(1):61-79.
[54]Ammann P, Wei D, Xu D. Using a model checker to test safety properties[C]. Proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems, Skovde, Sweden:IEEE Computer Society,2001:212-221.
[55]Potter B, Mcgraw G. Software security testing[J]. Security & Privacy, IEEE,2004,2(5): 81-85.
[56]Zelkowitz M V, Rus I. Understanding Ⅳ & Ⅴ in a safety critical and complex evolutionary environment:the NASA space shuttle program[C]. Proceedings of the 23rd International Conference on Software Engineering, Toronto, Ontario, Canada:IEEE Computer Society, 2001:349-357.
[57]Littlewood B, Wright D. Some conservative stopping rules for the operational testing of safety-critical software[J]. IEEE Transactions on Software Engineering,1997,23(11): 673-683.
[58]Auguston M, Michael J B, Shing M T. Environment behavior models for automation of testing and assessment of system safety[J]. Information and Software Technology,2006, 48(10):971-980.
[59]Kapoor K, Bowen J P. A formal analysis of MCDC and RCDC test criteria[J]. Software Testing, Verification and Reliability,2005,15(1):21-40.
[60]Lau M F, Yu Y T. An extended fault class hierarchy for specification-based testing[J]. ACM Trans on Software Engineering and Methodology,2005,14(3):247-276.
[61]Gargantini A. Using model checking to generate fault detecting tests[C]. Proceedings of the Conference of TAP'2007:Springer Berlin/Heidelberg,2007:189-206.
[62]单锦辉,高友峰,刘明浩.一种新的变异测试数据自动生成方法[J].计算机学报,2008,31(6)：1025—1034.
[63]陈璇.浅谈关于软件安全性测试方法研究[J].电脑知识与技术,2009,5(9)：2148-2149.
[64]屠海滢,吴芳美.面向软件黑箱测试的仿真环境嵌入故障研究[J].软件学报,1999,10(5)：516-520.
[65]Morell L J. A theory of fault-based testing[J]. IEEE Transactions on Software Engineering, 1990,16(8):844-857.
[66][66] Bernhard K A, Carlo C D. From faults via test purposes to test cases:on the fault-based testing of concurrent systems[C]. Proceedings of the Conference on Fundamental Approaches to Software Engineering-FASE,2006:324-338.
[67]Wimmel G, Jurjens J. Specification-based test generation for security-critical systems using mutations [C]. Proceedings of the 4th International Conference on Formal Engineering Methods:Formal Methods and Software Engineering, Shanghai, China:Springer-Verlag, 2002:471-482.
[68]Da Silva D A, Machado P D L. Towards test purpose generation from CTL properties for reactive systems[J]. Electronic Notes in Theoretical Computer Science,2006,164(4):29-40.
[69]Seungjae H, Shin K G, Rosenberg H A. DOCTOR:an integrated software fault Injection Environment[C]. Proceedings of the International Conference on Computer Performance and Dependability Symposium, ErlangEn:IEEE Computer Society,1995:204-213.
[70]Kanawati G A, Kanawati N A, Abraham J A. FERRARI:A flexible software-based fault and error injection system[J]. IEEE Transactions on Computers,1995,44(2):248-260.
[71]常庆,陈建辉,邱鹏.FTA在故障注入系统中的应用研究[J].仪表技术,2007,(12)：51—53.
[72]Sanchez M A, Felder M A. A systematic approach to generate test cases based on faults[C]. Proceedings of the Conference on Argentine Symposium in Software Engineering, Buenos Aires,2003:1-16.
[73]De Vries R G. Towards formal test purposes[C]. Proceedings of the Conference on Formal Approaches to Testing of Software 2001 (FATES'01), Aarhus:Kluwer Academic Publisher, 2001:61-76.
[74]Boyer R, Elspas B, Levitt K. SELECT--a formal system for testing and debugging programs by symbolic execution[J]. ACM SIGPLAN Notices,1975,10(6):234-245.
[75]Ferguson R, Korel B. The chaining approach for software test data generation[J]. ACM Transactions on Software Engineering and Methodology,1996,5(1):63-86.
[76]Zhang J, Wang X. A constraint solver and its application to path feasibility analysis[J]. International journal of software engineering and knowledge engineering,2001,11(2): 139-156.
[77]Zhang J, Xu C, Wang X. Path-oriented test data generation using symbolic execution and constraint solving techniques[C]. Proceedings of the Second International Conference on Software Engineering and Formal Methods, Washington:IEEE Computer Society, 2004:242-250.
[78]Myers G. The art of software testing[M]. New York:Wiley,1979.
[79]Ammann P, Black P E. Abstracting formal specifications to generate software tests via model checking[C]. Proceedings of the 18th Digital Avionics Systems Conference (DASC), St. Louis, Missouri:IEEE Computer Society,1999:1-10.
[80]Calame J R, Ioustinova N, Van De Pol J. Automatic model-based generation of parameterized test cases using data abstraction[J]. Electronic Notes in Theoretical Computer Science,2007,191(1):25-48.
[81]Fraser G, Wotawa F, Ammann P. Issues in using model checkers for test case generation[J]. Journal of Systems and Software,2009,82(9):1403-1418.
[82]Zhang Y, Zhao X Q, Zheng W, et al. System safety property-oriented test sequences generating method based on model checking[J]. WIT Transactions on the Built Environment, 2010,144(3):747-759.
[83]Aboelfotoh H, Abou-Rabia O, Ural H. A test generation algorithm for systems modelled as non-deterministic FSMs[J]. Software Engineering Journal,1993,8(4):184-188.
[84]Gargantini A, Heitmeyer C. Using model checking to generate tests from requirements specifications[J]. ACM SIGSOFT Software Engineering Notes,1999,24(6):146-162.
[85]Ammann P E, Black P E, Majurski W. Using model checking to generate tests from specifications [C]. Proceedings of the Second IEEE International Conference on Formal Engineering Methods, Brisbane, Queensland, Australia:IEEE Computer Society, 1998:46-54.
[86]Hartmann J, Imoberdorf C, Meisinger M. UML-based integration testing[J]. ACM SIGSOFT Software Engineering Notes,2000,25(5):60-70.
[87]Friedman G, Hartman A, Nagin K, et al. Projected state machine coverage for software testing[J]. ACM SIGSOFT Software Engineering Notes,2002,27(4):134-143.
[88]Tracey N, Clark J, Mcdermid J, et al. A search-based automated test-data generation framework for safety-critical systems[C]. Proceedings of the Conference on Systems Engineering for Business Process Change, New York:Springer-Verlag,2002:174-213.
[89]Goodenough J B, Gerhart S L. Toward a theory of test data selection[J]. ACM SIGPLAN Notices,1975,10(6):493-510.
[90]Amla N, Ammann P. Using Z specifications in category partition testing[C]. Proceedings of the Seventh Annual Conference on Computer Assurance, Gaithersburg MD:IEEE Computer Society,1992:3-10.
[91]Ammann P, Offutt J. Using formal methods to derive test frames in category-partition testing[C]. Proceedings of the Ninth Annual Conference on Computer Assurance, Gaithersburg, Maryland:IEEE Computer Society,1994:69-79.
[92]Ostrand T J, Balcer M J. The category-partition method for specifying and generating factional tests[J]. Communications of the ACM,1988,31(6):676-686.
[93]Cohen D, Society C, Dalal S, et al. The AETG system:an approach to testing based on combinatorial design[J]. IEEE Transactions on Software Engineering,1997,23(7):437-444.
[94]Malekzadeh M, Ainon R N. An automatic test case generator for testing safety-critical software systems[C]. Proceedings of the 2nd International Conference on Computer and Automation Engineering, Singapore,2010:163-167.
[95]Ali S, Briand L C, Rehman M J-U, et al. A state-based approach to integration testing based on UML models[J]. Information and Software Technology,2007,49(11):1087-1106.
[96]Barnett M, Grieskamp W, Nachmanson L, ct al. Model-based testing with AsmL.NET[C]. Proceedings of the 1st European Conference on Model-Driven Software Engineering, Nuremberg, Germany:Information Society,2003:1-12.
[97]De Vries R G, Tretmans J. On-the-fly conformance testing using SPIN[J]. International Journal on Software Tools for Technology Transfer (STTT),2000,2(4):382-393.
[98]Gargantini A, Riccobene E, Rinzivillo S. Using spin to generate tests from ASM specifications[C]. Proceedings of the 10th International Conference on Advances in Theory and Practice, Taormina, Italy:Springer Berlin/Heidelberg,2003:263-277.
[99]李书浩,王戟,齐治昌.一种面向性质的实时系统测试方法[J].电子学报,2005,33(5)：827—834.
[100]Fernandez J C, Mounier L, Pachon C. Property oriented test case generation[C]. Proceedings of the 3rd International Workshop on Formal Approaches to Testing of Software, Montreal, Quebec:Springer-Verlag,2003:147-163.
[101]Rusu V, Marchand H, Jeron T. Verification and symbolic test generation for safety properties[R]. France:Institut National De Recherche En Informatique Et En Automatique, 2004.
[102]Camille C. Integrating formal verification and conformance testing for reactive systems[J]. IEEE Transactions on Software Engineering,2007,33(8):558-574.
[103]Mingsong C, Mishra P. Functional test generation using efficient property clustering and learning techniques[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2010,29(3):396-404.
[104]Alexander P, Heiko L, Jan P. Model based testing in incremental system development[J]. Journal of Systems and Software,2004,70(3):315-329.
[105]Alexander P, Heiko L. Model based testing with constraint logic programming:first results and challenges [C]. Proceedings of the 2th International Workshop on Automated Program Analysis, Testing and Verification, Washington, DC, USA:IEEE Computer Society, 2001:1-9.
[106]Jard C, Jeron T. TGV:theory, principles and algorithms A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems[J]. International Journal on Software Tools for Technology Transfer,2005,7(4):297-315.
[107]吴鹏.并发系统的模型检测与测试[D].北京：中国科学院,2005.
[108]Beat K, Jens G, Dieter H, et al. Autolink-a tool for automatic test generation from SDL specifications[C]. Proceedings of the IEEE International Workshop on Industrial Strength Formal Specification Techniques (WIFT98), Florida:IEEE Computer Society,1998:114-125.
[109]Fraser G, Wotawa F. Test-case generation and coverage analysis for nondeterministic systems using model-checkers[C]. Proceedings of the International Conference on Software Engineering Advances, Cap Esterel, French Riviera, France:IEEE Computer Society, 2007:45-50.
[110]Belli F, Giildali B. A holistic approach to test-driven model checking[C]. Proceedings of the 18th International Conference on Innovations in Applied Artificial Intelligence, Bari, Italy: Springer-Verlag,2005:321-331.
[111]Callahan J, Schneider F, Easterbrook S. Automated software testing using model-checking[C]. Proceedings of the of 1996 SPIN Workshop, New Jersey: Springer-Verlag,1996.
[112]Engels A, Feijs L, Mauw S. Test generation for intelligent networks using model checking[C]. Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Netherlands:Springer-Verlag,1997:384-398.
[113]Calvagna A, Gargantini A. A logic-based approach to combinatorial testing with constraints tests and proofs[C]. Proceedings of the 2nd International Conference on Tests and Proofs, Prato, Italy:Springer Berlin,2008:66-83.
[114]Heimdahl M P E, Rayadurgam S, Visscr W. Specification centered testing[C]. Proceedings of the Second International Workshop on Automated Program Analysis, Testing and Verification (ICSE 2001), Toronto, Ontario, Canada:IEEE Computer Society,2001:1-5.
[115]Hong H S, Cha S D, Lee I, et al. Data flow testing as model checking[C]. Proceedings of the 25th International Conference on Software Engineering, Washington,DC,USA:IEEE Computer Society,2003:232-242.
[116]Hamon G, De Moura L, Rushby J. Generating efficient test sets with a model checker[C]. Proceedings of the Second International Conference on Software Engineering and Formal Methods (SEFM), Los Alamitos, CA, USA:IEEE Computer Society,2004:261-270.
[117]Black P E. Modeling and marshaling:making tests from model checker counterexamples[C]. Proceedings of the 19th Digital Avionics Systems Conference, Philadelphia, PA, USA:IEEE Computer Society,2000:31-36.
[118]Tan L, Sokolsky O, Lee I. Specification-based testing with linear temporal logic[C]. Proceedings of the International Conference on Information Reuse and Integration, Las Vegas, NV, USA:IEEE Computer Society,2004:493-498.
[119]Vadim O, Paul E B, Yaacov Y. Testing with model checker:insuring fault visibility[J]. WSEAS Transactions on Systems,2003,2(1):77-82
[120]Fraser G, Wotawa F. Using model-checkers to generate and analyze property relevant test-cases[J]. Software Quality Journal,2008,16(2):161-183.
[121]Harrold M J, Gupta R, Soffa M L. A methodology for controlling the size of a test suite[J]. ACM SIGSOFT Software Engineering Notes,1993,2(3):270-285.
[122]程亮,张阳,冯登国.一种基于安全状态转移的简并测试集生成方法[J].软件学报,2010,21(3)：539-547.
[123]Ammann P, Black P E. A specification-based coverage metric to evaluate test sets[C]. Proceedings of the 4th IEEE International Symposium on High-Assurance Systems Engineering, Washington, DC, USA:IEEE Computer Society,1999:239-248.
[124]Giannakopoulou D, Havelund K. Automata-based verification of temporal properties on running programs[C]. Proceedings of the 16th IEEE International Conference on Automated Software Engineering, Washington, DC, USA:IEEE Computer Society,2001:412-416.
[125]Havelund K, Rosu G. Monitoring programs using rewriting[C]. Proceedings of the 16th IEEE International Conference on Automated Software Engineering, Washington, DC, USA:IEEE Computer Society,2001:135-143.
[126]Havelund K, Rosu G. Monitoring java programs with java PathExplorer[J]. Electronic Notes in Theoretical Computer Science,2001,55(2):200-217.
[127]Havelund K, Rosu G. Efficient monitoring of safety properties [J]. International Journal on Software Tools for Technology Transfer,2004,6(2):158-173.
[128]Rosu G, Havelund K. Rewriting-based techniques for runtime verification[J]. Automated Software Engineering,2005,12(2):151-197.
[129]Fraser G, Wotawa F. Using LTL rewriting to improve the performance of model-checker based test-case generation[C]. Proceedings of the 3rd International Workshop on Advances in Model-based Testing, New York, NY, USA:ACM Press,2007:64-74.
[130]Wijesekera D, Ammann P, Sun L, et al. Relating counterexamples to test cases in CTL model checking specifications[C]. Proceedings of the 3rd International Workshop on Advances in Model-based Testing, London, United Kingdom:ACM,2007:75-84.
[131]黄传动.通信协议的分布式测试方法研究和测试系统实现[D].合肥：中国科学技术大学,2000.
[132]蒋凡,宁华中.基于标号变迁系统的测试集自动生成[J].计算机研究与发展,2001,38(12)：1435-1445.
[133]Tretmans J. Conformance testing with labelled transition systems:Implementation relations and test generation[J]. Computer Networks and ISDN Systems,1996,29(1):49-79.
[134]Rusu V, Marchand H, Tschaen V, et al. From safety verification to safety testing[C]. Proceedings of the Conference on Testing of Communicating Systems, Oxford, UK:Springer, 2004:160-176.
[135]Abramsky S. Observation equivalence as a testing equivalence[J]. Theoretical Computer Science,1987,53(2-3):225-241.
[136]Lcduc G. A framework based on implementation relations for implementing LOTOS specifications[J]. Computer Networks and ISDN Systems,1992,25(1):23-41.
[137]Tretmans G J. A formal approach to conformance testing[D]. Enschede:University of Twente, 1992.
[138]古天龙.网络协议的形式化分析与设计[M].北京：电子工业出版社,2003.
[139]张轶.并发传值进程模型检测工具的数据类型扩展[D].北京：中国科学院,2003.
[140]Wu P, Zhang D. Compositional analysis of mobile IP with symbolic transition graphs[C]. Proceedings of the Conference of ICCC2004, Beijing, China,2004:1481-1488.
[141]Rothermel G, Untch R H, Chu C, et al. Test case prioritization:an empirical study[C]. Proceedings of the IEEE International Conference on Software Maintenance, Washington, DC, USA:IEEE Computer Society,1999:179-188.
[142]Lbaum S, Malishevsky A, Rothermel G. Incorporating varying test costs and fault severities into test case prioritization[C]. Proceedings of the 23rd International Conference on Software Engineering, IEEE Computer Society:Washington, USA,2001:329-338.
[143]Fraser G, Wotawa F. Test-case prioritization with model-checkers[C]. Proceedings of the 25th LASTED International Conference on Software Engineering, Anaheim, CA, USA:ACTA Press,2007:267-272.
[144]唐涛,徐田华,赵林.列车运行控制系统规范建模与验证[M].北京：中国铁道出版社,2010.
[145]Clarke E M, Grumberg O, Mcmillan K L, et al. Efficient generation of counterexamples and witnesses in symbolic model cheeking[C]. Proceedings of the 32nd annual ACM/IEEE Design Automation Conference, San Francisco, California, United States:ACM, 1995:427-432.
[146]Design/CPN ASK-CTL manual[EB/OL] (1996)[1996]. http://www.daimi.au.dk/design CPN/libs/askctl/ASKCTLmanual.pdf.
[147]Katsaros P. A roadmap to electronic payment transaction guarantees and a Colored Petri Net model checking approach[J]. Information and Software Technology,2009,51(2):235-257.
[148]Heintze N, Tygar J D, Wing J, et al. Model checking electronic commerce protocols [C]. Proceedings of the 2nd USENIX Workshop on Electronic Commerce, Oakland, California: USENIX Association,1996:1-10.
[149]Grabowski J. Test case generation and test case specification based on message sequence charts[D]. Gottingen:University of Gottingen,1994.
[150]Fernandez J C, Jard C, Jeron T. An experiment in automatic generation of test suites for protocols with verification technology[J]. Science of Computer Programming,1997,29(1-2): 123-146.
[151]Berard B, Bidoit M, Finkel A, et al. Systems and software verification model checking techniques and tools[M]. Berlin:Springer-Verlag,2001.
[152]Zhang Y, Tang T, Huang Q, et al. The test of train control system based on Colored Petri Net[C]. Proceedings of the 9th World Congress on Intelligent Control and Automation, Taipei:IEEE Computer Society,2011:315-320.
[153]门鹏,段振华.着色Petri网模型检测工具的扩展及其在Web服务组合中的应用[J].计算机研究与发展,2009,46(8)：1294—1303.
[154]吴建平.基于形式化方法的协议测试理论[J].清华大学学报(自然科学版),2001,41(4)：203—208.
[155]Wu P. Analyzing interoperability of protocols using model checking[J]. Chinese Journal of Electronics,2005,14(3):453-457.
[156]Allan C, Christensen S, Mortensen K H. Model checking coloured petri nets exploiting srongly connected components[C]. Proceedings of the International Workshop on Discrete Event Systems, Scotland, UK:Edinburgh,1997:169-177.
[157]祝颂和.离散数学[M].西安：西安交通大学出版社,1991.
[158]Meyer H M, Schnieder E. Modelling and simulation of train control systems using petri nets[C]. Proceedings of the World Congress on Formal Methods in the Development of Computing Systems, Toulouse:Springer,1999:1867-1883.
[159]Meyer M H, Schnieder E. Modeling train control systems with Petri nets-A functional reference-architecture[C]. Proceedings of the 2000 IEEE International Conference on System, man and Cybernetics, Nashville, TN, USA:IEEE Computer Society,2000:3081-3086.
[160]Andrade W, Machado P. Testing interruptions in reactive systems [J]. Formal Aspects of Computing,2011,22(1):1-23.
[161]Yatake K, Aoki T. Automatic generation of model checking scripts based on environment modeling[C]. Proceedings of the 17th International SPIN Conference on Model Checking Software, Enschede, The Netherlands:Springer-Verlag,2010:58-75.
[162]Peleska J, Siegel M. Test automation of safety-critical reactive systems[J]. South African Computer Journal,1997,19:53-77.
[163]Zhang Y, Tang T, Li K P, et al. Formal verification of safety protocol in train control system[J]. Science China Technological Sciences,2011,54(11):3078-3090.
[164]Watanabe H, Kudoh T. Test suite generation methods for concurrent systems based on coloured Petri nets[C]. Proceedings of the Conference of Asia Pacific Software Engineering, Brisbane, Australia:IEEE Computer Society,1995:242-251.
[165]Nicola R D, Vaandrager F. Three logics for branching bisimulation[J]. Journal of the ACM, 1995,42(2):458-487.
[166]Clarke E M, Grumberg O, Peled D A. Model checking[M]. CamBridge:MIT Press,2001.
[167]Park I. Fault properties and their uses in testing digital integrated circuits[D]. California: Stanford University,2009.
[168]Kuhn D R. Fault classes and error detection capability of specification-based testing[J]. ACM Transactions on Software Engineering and Methodology,1999,8(4):411-424.
[169]Tsuchiya T, Kikuno T. On fault classes and error detection capability of specification-based testing[J]. ACM Transactions on Software Engineering and Methodology,2002,11(1): 58-62.
[170]Okun V, Black P E, Yesha Y. Comparison of fault classes in specification-based testingfj]. Information and Software Technology,2004,46(8):525-533.
[171]Du W, Mathur A. Vulnerability testing of software system using fault injection[R]. West Lafayette:Purdue University,1998.
[172]ERTMS UNISIG. SUBSET-088-2003. ETCS application levels 1 & 2-safety analysis, Version 2.2.2[S]. EU:ERTMS,2003.
[173]Murphy G, Notkin D, Sullivan K. Software reflexion models:bridging the gap between source and high-level models[C]. Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, Washington, D.C., United States:ACM,1995:18-28.
[174]张曙光CTCS-3级列控系统总体技术方案[M].北京：中国铁道出版社,2008.
[175]刘绍国,张岩,翟飞飞.基于UML顺序图的多播报文安全确认方式设计[J].中国新通信,2008,(19)：42—44.
[2]Papadopoulos Y, Mcdermid. The potential for a generic approach to certification of safety critical systems in the transportation sector[J]. Reliability Engineering & System Safety, 1999,63(1):47-66.
[3]孟庆宇.尼崎事故的反思[J].铁道知识,2006,(4)：24-25.
[4]徐应诗,刘斌,阮镰.基于故障注入的仿真测试方法过程框架[J].测控技术,2007,26(10)：50-56.
[5]CENELEC. EN50128--2011. Railway application-communications, signaling and processing systems-software for railway control and protection systems[S]. UK:CENELEC, 2011.
[6]陈锦富,卢炎生,谢晓东.软件错误注入测试技术研究[J].软件学报,2009,20(6)：1425—1443.
[7]张岩,唐涛,燕飞.CBTC数据通信系统性能分析模型及应用研究[J].铁道学报,2011,33(5)：60-65.
[8]Zhang Y, Zhu L, Chen L, et al. A method for simulation and analysis of trackside data communication system in CBTC[C]. Proceedings of the 2009 International Conference on Communications and Mobile Computing Kunming:IEEE Computer Society,2009:529-533.
[9]宋沛东,张勇.CTCS3仿真测试平台一RBC仿真子系统的设计与实现[J].中国科技信息,2008,(1)：100—103.
[10]铁道部科技司CTCS-3级列控系统标准规范-CTCS-3级列控系统系统需求规范(SRS) [M].北京：中国铁道出版社,2009.
[11]Eliane M, Ana M A. ATIFS:a testing toolset with software fault injection[C]. Proceedings of the Conference of York Computer Science Yellow Report 2003, UK:Department of Computer Science at York,2003:1-3.
[12]Jonas B. Early fault detection with model-based testing[C]. Proceedings of the 7th ACM SIGPLAN workshop on ERLANG, Victoria, BC, Canada:ACM Press,2008:9-20.
[13]Hierons R, Bogdanov K, Bowen J, et al. Using formal specifications to support testing[J]. ACM Computing Surveys,2009,41(2):1-76.
[14]Offutt J, Liu S, Abdurazik A, et al. Generating test data from state-based specifications[J]. The Journal of Software Testing, Verification and Reliability,2003,13(1):25-53.
[15]吴芳美.铁路安全软件测试评估[M].北京：中国铁道出版社,2001.
[16]张岩,唐涛,马连川.基于交换式以太网安全通信协议的模型和仿真研究[J].铁道学报,2010,32(3)：43—48.
[17]Raymond P, Nicollin X, Halbwachs N, et al. Automatic testing of reactive systems[C]. Proceedings of the 19th IEEE Conference of Real-Time Systems Symposium, Madrid, Spain: IEEE Computer Society,1998:200-209.
[18]Grard B, Georges G. The ESTEREL synchronous programming language:design, semantics, implementation[J]. Science of Computer Programming,1992,19(2):87-152.
[19]Caspi P, Pilaud D, Halbwachs N, et al. LUSTRE:a declarative language for programming synchronous systems[C]. Proceedings of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, West Germany:ACM Press,1987:178-188.
[20]Le Guernic P, Benveniste A, Bournai P, et al. Signal-A data flow-oriented language for signal processing[J]. Acoustics, Speech and Signal Processing, IEEE Transactions on,1986,34(2): 362-374.
[21]Apirukvorapinit P. Search-based approach of automated test generation for state-based components[D]. Chicago, IL, USA:Illinois Institute of Technology,2005.
[22]燕飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D].北京：北京交通大学,2006.
[23]马均飞,郑文强.软件测试设计[M].北京：电子工业出版社,2011.
[24]徐中伟,吴芳美.形式化故障树分析建模和软件安全性测试[J].同济大学学报(自然科学版),2001,29(11)：1299—1302.
[25]Tommaso P D, Flammini F, Lazzaro A, et al. The simulation of anomalies in the functional testing of the ERTMS/ETCS trackside system[C]. Proceedings of the 9th IEEE International Symposium on High-Assurance Systems Engineering, Heidelberg, Germany:IEEE Computer Society,2005:131-139.
[26]喻钢,熊静,徐中伟.通用的安全苛求软件安全性测试方法[J].计算机工程,2010,36(17)：28-29.
[27]喻钢,徐中伟,杜军威.场景一事件驱动的安全苛求软件系统仿真测试脚本语言研究[J].计算机应用,2010,30(2)：374-379.
[28]章文婷,徐中伟,喻刚.面向安全苛求软件的测试用例自动生成[J].计算机应用研究,2009,26(1)：140—142+174.
[29]周绍君,徐中伟,喻钢.面向安全需求的测试用例自动生成技术研究[J].计算机工程与应用,2009,45(28)：75—78.
[30]ERTMS UNISIG SUBSET 076-2--2003. Methodology to prepare features, Version 2.2.2[S]. EU:ERTMS,2003.
[31]ERTMS UNISIG. SUBSET 076-3--2003 Methodology of testing, Version 2.2.2[S]. EU: ERTMS,2003.
[32]ERTMS UNISIG. SUBSET076-4-1--2003. Test sequence generation:methodology and rules, Version 2.2.2[S]. EU:ERTMS 2003.
[33]ERTMS UNISIG. SUBSET-094-0--2003. Functional requirements for an on board reference test facility,Version 1.0.0[S]. EU:ERTMS,2003.
[34]季学胜,李开成,张勇.CTCS-3级列控系统测试案例生成方法的研究[J].铁道通信信号,2009,45(10)：1—5.
[35]王春花.无线闭塞中心的测试方法研究[D].北京：北京交通大学,2008.
[36]De Nicola G, Di Tommaso.P, Esposito R, et al. A hybrid testing methodology for railway control systems[J]. Lecture Notes in Computer Science,2004,3219:116-129.
[37]Lee J D, Jung J I, Lee J H, et al. Verification and conformance test generation of communication protocol for railway signaling systems[J]. Computer Standards & Interfaces, 2007,29(2):143-151.
[38]Lee J H, Hwang J G, Shin D, et al. Development of verification and conformance testing tools for a railway signaling communication protocol[J]. Computer Standards & Interfaces, 2009,31(2):362-371.
[39]章慧,张勇.CTCS3级列控系统车载设备测试方法研究[J].铁路计算机应用,2008,17(4)：23-27.
[40]张勇,于超琦.CTCS-3级列控系统车载设备测试序列优化生成方法[J].中国铁道科学,2011,32(3)：100—106.
[41]赵显琼,唐涛.多端口形式化测试自动生成方法在CTCS-3车载系统中的应用[J].铁道学报,2011,33(7)：44-51.
[42]赵显琼,李开成,唐涛.基于TTCN-3的CTCS-3级列车运行控制系统自动测试方法[J].铁道通信信号,2010,46(7)：15-20.
[43]Angeletti D, Giunchiglia E, Narizzano M, et al. Using bounded model checking for coverage analysis of safety-critical software in an industrial setting[J]. Journal of Automated Reasoning,2010,45(4):397-414.
[44]李弋强,徐中伟,喻钢.面向安全需求的安全通信协议测试序列生成算法[J].计算机应用,2009,29(7)：1828-1831+1848.
[45]Tretmans J. Testing concurrent systems:a formal approach[C]. Proceedings of the 10th International Conference on Concurrency Theory, Eindhoven, Netherlands:Springer-Verlag, 1999:46-65.
[46]Medikonda B S, Panchumarthy S R. An approach to modeling software safety in safety-critical systems[J]. Journal of Computer Science,2009,5(4):311-322.
[47]Flammini F. Dependability assurance of real-time embedded control systems[M]. New York: Nova Science Publishers,2010.
[48]IEC. IEC 61508--1998. Functional safety of electrical/electronic/programmable electronic safety-related systems[S]. IEC,1998.
[49]Susannc K, Raimund K, Peter P. Development of a framework for automated systematic testing of safety-critical embedded systems[C]. Proceedings of the 2006 International Workshop on Intelligent Solutions in Embedded Systems, Vienna:IEEE Computer Society, 2006:1-13.
[50]Tracey N, Clark J, Mcdermid J, et al. Integrating safety analysis with automatic test-data generation for software safety verification[C]. Proceedings of the Conference of 17th International System Safety, Orlando, FL:System Safety Society,1999:128-137.
[51]Rayadurgam S. Automatic test-case generation from formal models of software[D]. Minnesota:University of Minnesota,2004.
[52]Rayadurgam S, Heimdahl M P E. Coverage based test-case generation using model checkers[C]. Proceedings of the 8th Annual IEEE International Conference on the Engineering of Computer Based Systems, Washington, DC, USA, USA:IEEE Computer Society,2001:83-91.
[53]Tracey N, Clark J, Mander K, et al. Automated test-data generation for exception conditions[J]. Software:Practice and Experience,2000,30(1):61-79.
[54]Ammann P, Wei D, Xu D. Using a model checker to test safety properties[C]. Proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems, Skovde, Sweden:IEEE Computer Society,2001:212-221.
[55]Potter B, Mcgraw G. Software security testing[J]. Security & Privacy, IEEE,2004,2(5): 81-85.
[56]Zelkowitz M V, Rus I. Understanding Ⅳ & Ⅴ in a safety critical and complex evolutionary environment:the NASA space shuttle program[C]. Proceedings of the 23rd International Conference on Software Engineering, Toronto, Ontario, Canada:IEEE Computer Society, 2001:349-357.
[57]Littlewood B, Wright D. Some conservative stopping rules for the operational testing of safety-critical software[J]. IEEE Transactions on Software Engineering,1997,23(11): 673-683.
[58]Auguston M, Michael J B, Shing M T. Environment behavior models for automation of testing and assessment of system safety[J]. Information and Software Technology,2006, 48(10):971-980.
[59]Kapoor K, Bowen J P. A formal analysis of MCDC and RCDC test criteria[J]. Software Testing, Verification and Reliability,2005,15(1):21-40.
[60]Lau M F, Yu Y T. An extended fault class hierarchy for specification-based testing[J]. ACM Trans on Software Engineering and Methodology,2005,14(3):247-276.
[61]Gargantini A. Using model checking to generate fault detecting tests[C]. Proceedings of the Conference of TAP'2007:Springer Berlin/Heidelberg,2007:189-206.
[62]单锦辉,高友峰,刘明浩.一种新的变异测试数据自动生成方法[J].计算机学报,2008,31(6)：1025—1034.
[63]陈璇.浅谈关于软件安全性测试方法研究[J].电脑知识与技术,2009,5(9)：2148-2149.
[64]屠海滢,吴芳美.面向软件黑箱测试的仿真环境嵌入故障研究[J].软件学报,1999,10(5)：516-520.
[65]Morell L J. A theory of fault-based testing[J]. IEEE Transactions on Software Engineering, 1990,16(8):844-857.
[66][66] Bernhard K A, Carlo C D. From faults via test purposes to test cases:on the fault-based testing of concurrent systems[C]. Proceedings of the Conference on Fundamental Approaches to Software Engineering-FASE,2006:324-338.
[67]Wimmel G, Jurjens J. Specification-based test generation for security-critical systems using mutations [C]. Proceedings of the 4th International Conference on Formal Engineering Methods:Formal Methods and Software Engineering, Shanghai, China:Springer-Verlag, 2002:471-482.
[68]Da Silva D A, Machado P D L. Towards test purpose generation from CTL properties for reactive systems[J]. Electronic Notes in Theoretical Computer Science,2006,164(4):29-40.
[69]Seungjae H, Shin K G, Rosenberg H A. DOCTOR:an integrated software fault Injection Environment[C]. Proceedings of the International Conference on Computer Performance and Dependability Symposium, ErlangEn:IEEE Computer Society,1995:204-213.
[70]Kanawati G A, Kanawati N A, Abraham J A. FERRARI:A flexible software-based fault and error injection system[J]. IEEE Transactions on Computers,1995,44(2):248-260.
[71]常庆,陈建辉,邱鹏.FTA在故障注入系统中的应用研究[J].仪表技术,2007,(12)：51—53.
[72]Sanchez M A, Felder M A. A systematic approach to generate test cases based on faults[C]. Proceedings of the Conference on Argentine Symposium in Software Engineering, Buenos Aires,2003:1-16.
[73]De Vries R G. Towards formal test purposes[C]. Proceedings of the Conference on Formal Approaches to Testing of Software 2001 (FATES'01), Aarhus:Kluwer Academic Publisher, 2001:61-76.
[74]Boyer R, Elspas B, Levitt K. SELECT--a formal system for testing and debugging programs by symbolic execution[J]. ACM SIGPLAN Notices,1975,10(6):234-245.
[75]Ferguson R, Korel B. The chaining approach for software test data generation[J]. ACM Transactions on Software Engineering and Methodology,1996,5(1):63-86.
[76]Zhang J, Wang X. A constraint solver and its application to path feasibility analysis[J]. International journal of software engineering and knowledge engineering,2001,11(2): 139-156.
[77]Zhang J, Xu C, Wang X. Path-oriented test data generation using symbolic execution and constraint solving techniques[C]. Proceedings of the Second International Conference on Software Engineering and Formal Methods, Washington:IEEE Computer Society, 2004:242-250.
[78]Myers G. The art of software testing[M]. New York:Wiley,1979.
[79]Ammann P, Black P E. Abstracting formal specifications to generate software tests via model checking[C]. Proceedings of the 18th Digital Avionics Systems Conference (DASC), St. Louis, Missouri:IEEE Computer Society,1999:1-10.
[80]Calame J R, Ioustinova N, Van De Pol J. Automatic model-based generation of parameterized test cases using data abstraction[J]. Electronic Notes in Theoretical Computer Science,2007,191(1):25-48.
[81]Fraser G, Wotawa F, Ammann P. Issues in using model checkers for test case generation[J]. Journal of Systems and Software,2009,82(9):1403-1418.
[82]Zhang Y, Zhao X Q, Zheng W, et al. System safety property-oriented test sequences generating method based on model checking[J]. WIT Transactions on the Built Environment, 2010,144(3):747-759.
[83]Aboelfotoh H, Abou-Rabia O, Ural H. A test generation algorithm for systems modelled as non-deterministic FSMs[J]. Software Engineering Journal,1993,8(4):184-188.
[84]Gargantini A, Heitmeyer C. Using model checking to generate tests from requirements specifications[J]. ACM SIGSOFT Software Engineering Notes,1999,24(6):146-162.
[85]Ammann P E, Black P E, Majurski W. Using model checking to generate tests from specifications [C]. Proceedings of the Second IEEE International Conference on Formal Engineering Methods, Brisbane, Queensland, Australia:IEEE Computer Society, 1998:46-54.
[86]Hartmann J, Imoberdorf C, Meisinger M. UML-based integration testing[J]. ACM SIGSOFT Software Engineering Notes,2000,25(5):60-70.
[87]Friedman G, Hartman A, Nagin K, et al. Projected state machine coverage for software testing[J]. ACM SIGSOFT Software Engineering Notes,2002,27(4):134-143.
[88]Tracey N, Clark J, Mcdermid J, et al. A search-based automated test-data generation framework for safety-critical systems[C]. Proceedings of the Conference on Systems Engineering for Business Process Change, New York:Springer-Verlag,2002:174-213.
[89]Goodenough J B, Gerhart S L. Toward a theory of test data selection[J]. ACM SIGPLAN Notices,1975,10(6):493-510.
[90]Amla N, Ammann P. Using Z specifications in category partition testing[C]. Proceedings of the Seventh Annual Conference on Computer Assurance, Gaithersburg MD:IEEE Computer Society,1992:3-10.
[91]Ammann P, Offutt J. Using formal methods to derive test frames in category-partition testing[C]. Proceedings of the Ninth Annual Conference on Computer Assurance, Gaithersburg, Maryland:IEEE Computer Society,1994:69-79.
[92]Ostrand T J, Balcer M J. The category-partition method for specifying and generating factional tests[J]. Communications of the ACM,1988,31(6):676-686.
[93]Cohen D, Society C, Dalal S, et al. The AETG system:an approach to testing based on combinatorial design[J]. IEEE Transactions on Software Engineering,1997,23(7):437-444.
[94]Malekzadeh M, Ainon R N. An automatic test case generator for testing safety-critical software systems[C]. Proceedings of the 2nd International Conference on Computer and Automation Engineering, Singapore,2010:163-167.
[95]Ali S, Briand L C, Rehman M J-U, et al. A state-based approach to integration testing based on UML models[J]. Information and Software Technology,2007,49(11):1087-1106.
[96]Barnett M, Grieskamp W, Nachmanson L, ct al. Model-based testing with AsmL.NET[C]. Proceedings of the 1st European Conference on Model-Driven Software Engineering, Nuremberg, Germany:Information Society,2003:1-12.
[97]De Vries R G, Tretmans J. On-the-fly conformance testing using SPIN[J]. International Journal on Software Tools for Technology Transfer (STTT),2000,2(4):382-393.
[98]Gargantini A, Riccobene E, Rinzivillo S. Using spin to generate tests from ASM specifications[C]. Proceedings of the 10th International Conference on Advances in Theory and Practice, Taormina, Italy:Springer Berlin/Heidelberg,2003:263-277.
[99]李书浩,王戟,齐治昌.一种面向性质的实时系统测试方法[J].电子学报,2005,33(5)：827—834.
[100]Fernandez J C, Mounier L, Pachon C. Property oriented test case generation[C]. Proceedings of the 3rd International Workshop on Formal Approaches to Testing of Software, Montreal, Quebec:Springer-Verlag,2003:147-163.
[101]Rusu V, Marchand H, Jeron T. Verification and symbolic test generation for safety properties[R]. France:Institut National De Recherche En Informatique Et En Automatique, 2004.
[102]Camille C. Integrating formal verification and conformance testing for reactive systems[J]. IEEE Transactions on Software Engineering,2007,33(8):558-574.
[103]Mingsong C, Mishra P. Functional test generation using efficient property clustering and learning techniques[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2010,29(3):396-404.
[104]Alexander P, Heiko L, Jan P. Model based testing in incremental system development[J]. Journal of Systems and Software,2004,70(3):315-329.
[105]Alexander P, Heiko L. Model based testing with constraint logic programming:first results and challenges [C]. Proceedings of the 2th International Workshop on Automated Program Analysis, Testing and Verification, Washington, DC, USA:IEEE Computer Society, 2001:1-9.
[106]Jard C, Jeron T. TGV:theory, principles and algorithms A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems[J]. International Journal on Software Tools for Technology Transfer,2005,7(4):297-315.
[107]吴鹏.并发系统的模型检测与测试[D].北京：中国科学院,2005.
[108]Beat K, Jens G, Dieter H, et al. Autolink-a tool for automatic test generation from SDL specifications[C]. Proceedings of the IEEE International Workshop on Industrial Strength Formal Specification Techniques (WIFT98), Florida:IEEE Computer Society,1998:114-125.
[109]Fraser G, Wotawa F. Test-case generation and coverage analysis for nondeterministic systems using model-checkers[C]. Proceedings of the International Conference on Software Engineering Advances, Cap Esterel, French Riviera, France:IEEE Computer Society, 2007:45-50.
[110]Belli F, Giildali B. A holistic approach to test-driven model checking[C]. Proceedings of the 18th International Conference on Innovations in Applied Artificial Intelligence, Bari, Italy: Springer-Verlag,2005:321-331.
[111]Callahan J, Schneider F, Easterbrook S. Automated software testing using model-checking[C]. Proceedings of the of 1996 SPIN Workshop, New Jersey: Springer-Verlag,1996.
[112]Engels A, Feijs L, Mauw S. Test generation for intelligent networks using model checking[C]. Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Netherlands:Springer-Verlag,1997:384-398.
[113]Calvagna A, Gargantini A. A logic-based approach to combinatorial testing with constraints tests and proofs[C]. Proceedings of the 2nd International Conference on Tests and Proofs, Prato, Italy:Springer Berlin,2008:66-83.
[114]Heimdahl M P E, Rayadurgam S, Visscr W. Specification centered testing[C]. Proceedings of the Second International Workshop on Automated Program Analysis, Testing and Verification (ICSE 2001), Toronto, Ontario, Canada:IEEE Computer Society,2001:1-5.
[115]Hong H S, Cha S D, Lee I, et al. Data flow testing as model checking[C]. Proceedings of the 25th International Conference on Software Engineering, Washington,DC,USA:IEEE Computer Society,2003:232-242.
[116]Hamon G, De Moura L, Rushby J. Generating efficient test sets with a model checker[C]. Proceedings of the Second International Conference on Software Engineering and Formal Methods (SEFM), Los Alamitos, CA, USA:IEEE Computer Society,2004:261-270.
[117]Black P E. Modeling and marshaling:making tests from model checker counterexamples[C]. Proceedings of the 19th Digital Avionics Systems Conference, Philadelphia, PA, USA:IEEE Computer Society,2000:31-36.
[118]Tan L, Sokolsky O, Lee I. Specification-based testing with linear temporal logic[C]. Proceedings of the International Conference on Information Reuse and Integration, Las Vegas, NV, USA:IEEE Computer Society,2004:493-498.
[119]Vadim O, Paul E B, Yaacov Y. Testing with model checker:insuring fault visibility[J]. WSEAS Transactions on Systems,2003,2(1):77-82
[120]Fraser G, Wotawa F. Using model-checkers to generate and analyze property relevant test-cases[J]. Software Quality Journal,2008,16(2):161-183.
[121]Harrold M J, Gupta R, Soffa M L. A methodology for controlling the size of a test suite[J]. ACM SIGSOFT Software Engineering Notes,1993,2(3):270-285.
[122]程亮,张阳,冯登国.一种基于安全状态转移的简并测试集生成方法[J].软件学报,2010,21(3)：539-547.
[123]Ammann P, Black P E. A specification-based coverage metric to evaluate test sets[C]. Proceedings of the 4th IEEE International Symposium on High-Assurance Systems Engineering, Washington, DC, USA:IEEE Computer Society,1999:239-248.
[124]Giannakopoulou D, Havelund K. Automata-based verification of temporal properties on running programs[C]. Proceedings of the 16th IEEE International Conference on Automated Software Engineering, Washington, DC, USA:IEEE Computer Society,2001:412-416.
[125]Havelund K, Rosu G. Monitoring programs using rewriting[C]. Proceedings of the 16th IEEE International Conference on Automated Software Engineering, Washington, DC, USA:IEEE Computer Society,2001:135-143.
[126]Havelund K, Rosu G. Monitoring java programs with java PathExplorer[J]. Electronic Notes in Theoretical Computer Science,2001,55(2):200-217.
[127]Havelund K, Rosu G. Efficient monitoring of safety properties [J]. International Journal on Software Tools for Technology Transfer,2004,6(2):158-173.
[128]Rosu G, Havelund K. Rewriting-based techniques for runtime verification[J]. Automated Software Engineering,2005,12(2):151-197.
[129]Fraser G, Wotawa F. Using LTL rewriting to improve the performance of model-checker based test-case generation[C]. Proceedings of the 3rd International Workshop on Advances in Model-based Testing, New York, NY, USA:ACM Press,2007:64-74.
[130]Wijesekera D, Ammann P, Sun L, et al. Relating counterexamples to test cases in CTL model checking specifications[C]. Proceedings of the 3rd International Workshop on Advances in Model-based Testing, London, United Kingdom:ACM,2007:75-84.
[131]黄传动.通信协议的分布式测试方法研究和测试系统实现[D].合肥：中国科学技术大学,2000.
[132]蒋凡,宁华中.基于标号变迁系统的测试集自动生成[J].计算机研究与发展,2001,38(12)：1435-1445.
[133]Tretmans J. Conformance testing with labelled transition systems:Implementation relations and test generation[J]. Computer Networks and ISDN Systems,1996,29(1):49-79.
[134]Rusu V, Marchand H, Tschaen V, et al. From safety verification to safety testing[C]. Proceedings of the Conference on Testing of Communicating Systems, Oxford, UK:Springer, 2004:160-176.
[135]Abramsky S. Observation equivalence as a testing equivalence[J]. Theoretical Computer Science,1987,53(2-3):225-241.
[136]Lcduc G. A framework based on implementation relations for implementing LOTOS specifications[J]. Computer Networks and ISDN Systems,1992,25(1):23-41.
[137]Tretmans G J. A formal approach to conformance testing[D]. Enschede:University of Twente, 1992.
[138]古天龙.网络协议的形式化分析与设计[M].北京：电子工业出版社,2003.
[139]张轶.并发传值进程模型检测工具的数据类型扩展[D].北京：中国科学院,2003.
[140]Wu P, Zhang D. Compositional analysis of mobile IP with symbolic transition graphs[C]. Proceedings of the Conference of ICCC2004, Beijing, China,2004:1481-1488.
[141]Rothermel G, Untch R H, Chu C, et al. Test case prioritization:an empirical study[C]. Proceedings of the IEEE International Conference on Software Maintenance, Washington, DC, USA:IEEE Computer Society,1999:179-188.
[142]Lbaum S, Malishevsky A, Rothermel G. Incorporating varying test costs and fault severities into test case prioritization[C]. Proceedings of the 23rd International Conference on Software Engineering, IEEE Computer Society:Washington, USA,2001:329-338.
[143]Fraser G, Wotawa F. Test-case prioritization with model-checkers[C]. Proceedings of the 25th LASTED International Conference on Software Engineering, Anaheim, CA, USA:ACTA Press,2007:267-272.
[144]唐涛,徐田华,赵林.列车运行控制系统规范建模与验证[M].北京：中国铁道出版社,2010.
[145]Clarke E M, Grumberg O, Mcmillan K L, et al. Efficient generation of counterexamples and witnesses in symbolic model cheeking[C]. Proceedings of the 32nd annual ACM/IEEE Design Automation Conference, San Francisco, California, United States:ACM, 1995:427-432.
[146]Design/CPN ASK-CTL manual[EB/OL] (1996)[1996]. http://www.daimi.au.dk/design CPN/libs/askctl/ASKCTLmanual.pdf.
[147]Katsaros P. A roadmap to electronic payment transaction guarantees and a Colored Petri Net model checking approach[J]. Information and Software Technology,2009,51(2):235-257.
[148]Heintze N, Tygar J D, Wing J, et al. Model checking electronic commerce protocols [C]. Proceedings of the 2nd USENIX Workshop on Electronic Commerce, Oakland, California: USENIX Association,1996:1-10.
[149]Grabowski J. Test case generation and test case specification based on message sequence charts[D]. Gottingen:University of Gottingen,1994.
[150]Fernandez J C, Jard C, Jeron T. An experiment in automatic generation of test suites for protocols with verification technology[J]. Science of Computer Programming,1997,29(1-2): 123-146.
[151]Berard B, Bidoit M, Finkel A, et al. Systems and software verification model checking techniques and tools[M]. Berlin:Springer-Verlag,2001.
[152]Zhang Y, Tang T, Huang Q, et al. The test of train control system based on Colored Petri Net[C]. Proceedings of the 9th World Congress on Intelligent Control and Automation, Taipei:IEEE Computer Society,2011:315-320.
[153]门鹏,段振华.着色Petri网模型检测工具的扩展及其在Web服务组合中的应用[J].计算机研究与发展,2009,46(8)：1294—1303.
[154]吴建平.基于形式化方法的协议测试理论[J].清华大学学报(自然科学版),2001,41(4)：203—208.
[155]Wu P. Analyzing interoperability of protocols using model checking[J]. Chinese Journal of Electronics,2005,14(3):453-457.
[156]Allan C, Christensen S, Mortensen K H. Model checking coloured petri nets exploiting srongly connected components[C]. Proceedings of the International Workshop on Discrete Event Systems, Scotland, UK:Edinburgh,1997:169-177.
[157]祝颂和.离散数学[M].西安：西安交通大学出版社,1991.
[158]Meyer H M, Schnieder E. Modelling and simulation of train control systems using petri nets[C]. Proceedings of the World Congress on Formal Methods in the Development of Computing Systems, Toulouse:Springer,1999:1867-1883.
[159]Meyer M H, Schnieder E. Modeling train control systems with Petri nets-A functional reference-architecture[C]. Proceedings of the 2000 IEEE International Conference on System, man and Cybernetics, Nashville, TN, USA:IEEE Computer Society,2000:3081-3086.
[160]Andrade W, Machado P. Testing interruptions in reactive systems [J]. Formal Aspects of Computing,2011,22(1):1-23.
[161]Yatake K, Aoki T. Automatic generation of model checking scripts based on environment modeling[C]. Proceedings of the 17th International SPIN Conference on Model Checking Software, Enschede, The Netherlands:Springer-Verlag,2010:58-75.
[162]Peleska J, Siegel M. Test automation of safety-critical reactive systems[J]. South African Computer Journal,1997,19:53-77.
[163]Zhang Y, Tang T, Li K P, et al. Formal verification of safety protocol in train control system[J]. Science China Technological Sciences,2011,54(11):3078-3090.
[164]Watanabe H, Kudoh T. Test suite generation methods for concurrent systems based on coloured Petri nets[C]. Proceedings of the Conference of Asia Pacific Software Engineering, Brisbane, Australia:IEEE Computer Society,1995:242-251.
[165]Nicola R D, Vaandrager F. Three logics for branching bisimulation[J]. Journal of the ACM, 1995,42(2):458-487.
[166]Clarke E M, Grumberg O, Peled D A. Model checking[M]. CamBridge:MIT Press,2001.
[167]Park I. Fault properties and their uses in testing digital integrated circuits[D]. California: Stanford University,2009.
[168]Kuhn D R. Fault classes and error detection capability of specification-based testing[J]. ACM Transactions on Software Engineering and Methodology,1999,8(4):411-424.
[169]Tsuchiya T, Kikuno T. On fault classes and error detection capability of specification-based testing[J]. ACM Transactions on Software Engineering and Methodology,2002,11(1): 58-62.
[170]Okun V, Black P E, Yesha Y. Comparison of fault classes in specification-based testingfj]. Information and Software Technology,2004,46(8):525-533.
[171]Du W, Mathur A. Vulnerability testing of software system using fault injection[R]. West Lafayette:Purdue University,1998.
[172]ERTMS UNISIG. SUBSET-088-2003. ETCS application levels 1 & 2-safety analysis, Version 2.2.2[S]. EU:ERTMS,2003.
[173]Murphy G, Notkin D, Sullivan K. Software reflexion models:bridging the gap between source and high-level models[C]. Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, Washington, D.C., United States:ACM,1995:18-28.
[174]张曙光CTCS-3级列控系统总体技术方案[M].北京：中国铁道出版社,2008.
[175]刘绍国,张岩,翟飞飞.基于UML顺序图的多播报文安全确认方式设计[J].中国新通信,2008,(19)：42—44.