摘要
随着列车运行控制系统的飞速发展,人们对于其能否安全可靠的完成承载运输任务越来越关注,而列控系统的可信性是否达到需求是影响这一点的关键。采用科学、系统的可信性验证方法对高速列控系统的复杂结构和功能进行可信性的验证是这一类系统设计开发过程不可缺少的环节。随着计算机技术的飞速发展,系统的结构复杂性、嵌入式特性和功能逻辑复杂性,给高速列控系统的可信性验证带来了极大的挑战。
论文针对高速列控系统的特点,在深入分析现有可信性验证方法侧重点和局限性的基础上,将可信性验证的内容确定为四个属性和两个部分。四个属性包括：可靠性,可用性,可维修性和安全性；两个部分包括：结构可信性验证和功能可信性验证。对基于嵌入式系统的高速列控系统来说,结构可信性是功能可信性的基础。本文针对当前列控系统结构可信性验证验证存在的问题,提出了多形式化语义融合方法,在对扩展参数化故障树(Extended Parametric Fault Tree, EPFT)、可维修故障树(Repairable Fault Tree, RFT)、混成马尔可夫链(Hybrid Morkov Chain, HMC和扩展有色Petri网(Extended Colored P etri Net, ECPN)四种方法进行融合后,得到混成马尔可夫——参数化可维修故障树(HMC-PRFT)结构可信性验证方法,为系统结构可信性验证提供了更加准确、高效的分析方法。针对功能可信性的重要组成——功能安全性,研究了功能安全性自动测试方法,提出了基于CPN模型和贝叶斯假设的功能安全性自动测试方法,通过概率描述的定量方式来反应系统功能是否达到安全需求,从而有效提高了测试效率,降低了测试负荷,同时也为系统安全性测试提供了理论支持。
论文的主要创新点如下：
(1)针对既有结构可信性验证方法的建模能力局限,包括复杂冗余策略建模能力局限和复杂维修策略建模能力局限,提出一种对参数化故障树的扩展机制,并运用这种机制将传统的“热备门”引入到参数化故障树中,扩展了参数化故障树的热备策略描述能力；提出了混成马尔可夫链维修策略描述方法；
(2)针对既有结构可信性验证方法的可信性数值计算困难的缺陷,扩展了有色Petri网的随机事件描述能力和数值计算能力；在此基础上,提出多形式化语义融合方法,得到HMC-PRFT结构可信性建模分析方法,提高了建模能力并实现了可信性数值计算；
(3)针对目前功能安全性测试内容不明确问题,提出了安全性自动测试方法,运用基于CPN的面向测试生成的建模方法和测试生成算法实现,包括：测试案例生成算法,功能测试序列及其输入域生成方法和诱导功能执行序列生成方法；
(4)针对目前功能安全性测试评判标准的不明确问题,提出了基于贝叶斯假设的功能SIL等级定量评价测试方法,针对无历史测试数据和有历史测试数据两种情况下,分别提出了与SIL等级对应的无失效通过的测试案例数目计算方法。
论文最后以中国列车运行控制系统第3级(CTCS-3)中的重要子系统——无线闭塞中心(Radio Block Center, RBC)子系统为例,采用HMC-PRFT方法完成其结构可信性验证,通过维修策略对比分析、部件可信性灵敏度分析和冗余策略可信性灵敏度分析对RBC系统结构设计提出了建议；采用基于CPN和贝叶斯假设的安全性自动测试方法,对RBC进行了功能安全性测试过程设计,通过这样的测试直接为RBC系统的安全性检验提供依据。
With the rapid development of the Train Control System, people are increasingly concerned about its ability to safe and reliable completion of the transport tasks, while its dependability reaches corresponding demand is the most important fact. Making use of scientific and systematic dependability verifying approaches to verify High-speed train control system both from structure and function is an indispensable component in the designing and development process of this type of system. With the fast development of computer technology, the complexity and embedded of the system brings a great challenge to the dependability verifying of high-speed train control system.
Based on the characteristics of high-speed train control system and the in-depth analysis of the focus and limitation of the existing dependability verifying approaches, this paper has determined that the content of dependability verification includes four attributes and two parts. Four attributes are reliability, availability, maintainability and safety; while two parts are structure dependability analysis and functional dependability test; while for the embedded high-speed train control system, structure dependability satisfied the demand is the basis of functional dependability test. Focus on the limitation of existing structure dependability analysis, this paper proposes a multi-formalism fusing approach, which fusing the following four formal methods:Extended Parametric Fault Tree (EPFT), Repairable Fault Tree (RFT), Hybrid Morkov Chain (HMC) and Extended Colored Petri Net (ECPN), and finally get the HMC-PRFT structure analysis approach which provide a more accurate and efficient analysis methods for the dependability analysis of system structure. Further focus on the important component of functional dependability--unctional safety, this article proposes the CPN and Bayesian assumption based functional SILs level quantitative evaluation testing approach, which makes use of probability to determine whether the functional safety requirements have been satisfied and effectively improve the efficiency of the test, reduce the test load, and provides a theoretical basis for the quantitative assessment of system safety.
The main innovations of this article are as follows:
(1) Focus on the limitation of traditional methods'modeling capabilities, including ccomplex redundancy strategy modeling capacity and complex repairing strategy modeling capacity, the study extends the modeling capability of parametric fault tree, and proposes hybrid Markov Chain for the complex repairing policy modeling;
(2) Against traditional methods cannot get the numerical results, the study extended the stochastic distribute description capability and numerical calculating capability of CPN. On this basis, the study proposes a multiformalism fusion method to get HMC-PRFT, which improves the modeling capabilities and implements the numerical calculating of system structure dependability.
(3) Focus on the uncertain contents of functional safety testing, this thesis proposes a safety quantitative evaluation testing method, which makes use of CPN to modeling and generating, including:test case generating algorithms, functional test sequences and input field generating algorithm and induction functional execution sequences generating method.
(4) Focus on the uncertain criteria of functional safety testing; this article proposes Bayesian assumption based SILs level quantitative evaluation testing method, which helps to calculating the required unfail passed test cases number under two different situations:with history testing data and without history testing data.
Finally in this thesis, the important subsystem of Chinese Train Control System Level3-Radio Block Center (RBC) is taken as a case study. HMC-PRFT method is implemented to analysis RBC structure dependability. Through the comparation of different repairing strategies, the components'sensitivity analysis and redundancy policy sensitivity analysis, give some recommendations to RBC system structure design; CPN and Bayesian assumption based functional safety quantitative evaluation testing method is used for test design of RBC functional safety assessment testing, provides proof for the safety inspection of the RBC system.
引文
[1]何积丰Cyber-Physical Systems中国计算机学会通讯.2010.6(1).25-29.
[2]Vicky Hartonas-Garmhausen, Sergio Campos, Alessandro Cimatti, etc.. Verification of a safety-critical railway interlocking system with real-time constraints. Science of Computer Programming.2000.36(1).458-463.
[3]Fangmei Wu, Meng Li. Railway Signaling Safety Testing Based on Dynamic Decision Table. Proceeding of'99ATS, IEEE Press,1999.247-250.
[4]IEC62278 Railway Application-The specification and demonstration of Reliability, Availability, Maintainability and Safety, RAMS. International Electrotechnical commission(IEC).2002.
[5]Neil R. Storey, Safety critical computer systems,Addison-Wesley Longman Publishing, Boston, MA, USA,1996.
[6]Software Safety, NASA Technical Standard,1997.http://satc.gsfc.nasa.gov/assure/distasst .pdf.
[7]W.S.Heath:Real-Time Software Techniques. Van Nostrand Reinhold, New York.1991.
[8]C.Laprie, Dependability:A unifying concept for reliable, safe, secure computing. In IFIP Congress,1992(1).585-593.
[9]Algirdas Avizienis, A., Lapric, J.C., Randell, B. Fundamental Concepts of Dependability. Research Report, Computer Science Dept, Univ. of California, Los Angeles,2001.
[10]Ioana Rus, Seijia Komi-Sirvio, and Patricia Cost. High Dependability Computing Program Software Dependability Properties:A Survey of Definitions, Measures and Techniques. Technical Report, Franhofer Center, Univ. of Maryland. January 2003.
[11]CENELEC. EN50126-1998 Railway applications:The specification and demonstration of reliability, availability, maintainability and safety (RAMS)[S]. Brussels.2001.
[12]Shigeto Hiraguri, Koji Iwata, Ikuo Watanabe. A Method of Evaluating Railway Signalling System Based on RAMS Concept. FORMS/FORMAT 2010, Part 2.97-105.
[13]http://www.uic.org/IMG/pdf/ERTMS_Regional_RAMS.pdf
[14]https://www.era.europa.eu/Document-Register/Documents/B 1-02s 1266-.pdf
[15]UNISIG. SUBSET-078:Failure Modes and Effects Analysis for the Interfaceto/from an Adjacent RBC-in Application Level 2,2009.
[16]肖伟赵嵩正.设备可靠性与维修决策关系研究.机械科学与技术.2004,Vol.22(5).111-114.
[17]员春欣.铁路信号容错技术.北京：中国铁道出版社,1997.
[18]Weinstein W W, Babcock P S, Frank Leong. Safety Analysis of ARES. October 1987.
[19]Colantuoni P, Firpo P, Ghiara T. Evaluation of the Effectiveness of RAMS Activities on the Design of Railway Transport Systems. Proceedings of the Probabilistic Safety Assessment and Management Conference. June 1996.832-839.
[20]Vinod Chandra. Reliability and Safety Analysis of Fault Tolerant and Fail Safe Node for Use in a Railway Signalling Systems. Reliability Engineering and System Safety, Vol.57,1997.177-183.
[21]Milutinovic Dusan, Lucanin Vojkan. Relation between reliability and availability of railway vehicles. FME Transactions,2005, vol.33.135-139.
[22]Ducko Shin, Kang-mi Lee, Jae-ho Lee. A development of the quantitative life span assessment model for the railroad signaling equipment.The International Conference on Electrical Engieering 2009.
[23]Ducko SHIN, Journal of the KSR. A Study on Reliability Prediction for Korea High Speed Train Control System,2006, vol.9(4).419-424.
[24]Yamamoto, M.; Takahashi, S.; Nakamura, H.. Dependability verification of architecture changed automatic train control system. Industrial Electronics,2001.Proceedings.ISIE 2001.2001, vol.1,417-422.
[25]Dobias, R.; Konarski, J.; Kubatova, H. Dependability Evaluation of Real Railway Interlocking Device. Digital System Design Architectures, Methods and Tools,2008.DSD'08.11th EUROMICRO Conference.2008.228-233.
[26]唐涛.LCF型列车超速防护系统可靠性设计.铁道学报(专辑),1995.36-40.
[27]赵明,宁宾,汀希时.列车超速防护系统的容错设计.铁道学报(专辑),vol.17,1995.14-19.
[28]惠永琴,汪希时.两种不同结构可修的ATP系统可靠性分析和比较.铁道学报(专辑)1995.41-47.
[29]惠永琴,汪希时.利用故障树方法分析LCF型系统中多机通信网络—容错BITBUS网络系统的可靠性.铁道学报(专辑),1995.63-69.
[30]高继祥.双机热备计算机联锁系统可靠性与安全性指标分析.北京交通大学学报,1998,vol.22(5).73-77.
[31]梅登华,周美玉.微机联锁系统的硬件及可靠性分析.西南交通大学学报,1997,vol.32(2).223-227.
[32]沈洁.三模冗余计算机联锁可靠性安全性分析.北京交通大学学报.1998,vol.22(5).111-114.
[33]邸丽清,袁湘鄂,王永年CTCS-3级列控系统RAM指标评价方法研究.中国铁道科学.2010,vol.31(6).92-96.
[34]Stefano Marrone. Modeling system reliability aspects of ERTMS/ETCS by Fault Trees and Bayesian Networks.In Proc. of 17th European Safety and Reliability Conference (ESREL),2006.
[35]G.K. Palshikar Safety checking in an automatic train operation system. Information and Software Technology 2001, vol.43.325-338.
[36]F. Belmonte, W. Schon, L. Heurley, R. Capel. Interdisciplinary safety analysis of complex socio-technological systems based on the functional resonance accident model:An application to railway tr afficsupervision. Reliability Engineering and System Safety 2011, vol.96.237-249.
[37]Z Armin, H Gunter. A train control system case study in model-based real time system design. In International parallel and distributed processing symposium, IEEE,2003.118-126
[38]H. Holger, N. J. David, S. U. Yaroslav. A Comparative Reliability Analysis ofETCS Train Radio Communications.AVACS Technical Report No.2.2005.
[39]Amendola, A.M.; Impagliazzo, L.; Marmo, P.; Poli, F.Experimental evaluation of computer-based railway control systems.Fault-Tolerant Computing.1997.380-384.
[40]Francesco Flammini, Model-based Dependability Evaluation of Complex Critical Control Systems.PhD. thesis.UNIVERSITA'DEGLI STUDI DI NAPOLI FEDERICO II,2006.
[41]Xu T H, Tang T, Gao C H, et al. Dependability analysis of the data communication system in train control system. Sci China Ser E-Tech Sci,2009, vol.52(9).2605-2618.
[42]上官伟等.基于故障注入的CTCS-3级列控系统可靠性评估技术研究.铁道通信信号.2010,vol.46(7).10-15.
[43]王俊峰,汪希时,赵会兵.青藏铁路列车运行控制系统的安全性分析.中国安全学报,2001,50(11).52-57
[44]王俊峰,张勇,程荫杭等.青藏铁路无线机车信号系统研究.铁道学报,2002,vol.24(3).112-117.
[45]Iyer R,Tang D.Measurement-based dependability evaluation of operational computer systems.Foundations of Dependable Computing,1994.vol.283.195-234.
[46]徐中伟.安全软件测试理论与技术的研究及其在铁路信号安全软件测评中的实现[博士论文],上海铁道大学,1998.
[47]虞翊.基于黑箱测试及风险分析的铁路信号控制软件安全性评估理论的研究与实践.[博士论文],上海铁道大学,2000.
[48]IEC 50(191)国际电技术词汇(IEV)——第191章：服务的可靠性与质量,1990.
[49]IEC 812系统可靠性分析技术——故障模式影响分析程序(FMEA),1985.
[50]IEC 1025故障树分析(FTA),1990.
[51]IEC 1078可信性分析技术——可靠性方框图方法,1991.
[52]IEC 60300-3-1可信性分析技术方法指南,1991.
[53]Retch J. L. Systems safety analysis:Failure mode and effect. National Safety News,1966.
[54]Bussolini J. J. High Reliability Design Techniques Applied to the Lunar Module, Lecture Series No.47 on Reliability on Avionics System.1971.
[55]King C. K., Rudd D. F. Design and Maintenance of Economical failure-tolerant process. American Institute Chemical Engineering Journal.1971, vol.18(1).257-269.
[56]Lees P. Less'Loss Prevention in the Process Industries.Elsevier,2005.
[57]Yamada K. Reliability Activities at Toyota Motor Company.JUSE.1977, vol.24(3).
[58]Henley J., Kumamoto H. Reliability Engineering and Risk Assessment.Englewood Clift, NJ: Prentice Hall,1981.
[59]Hassle. Advanced Concept in Fault Tree Analysis System Safety Symposium:Boeing/UW System Safety Symposium, A B Means,1965.
[60]Fussell J. B. Synthetic Tree Model, Report ANCR 1098 Aerojet Nuclear Company,1973.
[61]W. E. Vesely. Fault Tree Handbook, US Nuclear Regulatory Committee Report NUREG-0492.US NRC,1981.X.15-18.
[62]Sardella R. A Review of Knowledge-Based Systems for Fault Tree/Event Tree Construction,Tech. Note No.1.95.21.European Commission,1995.
[63]David John Puffery. The Principled Design of Computer System Safety Analyses[Dissertation]. University of York,1999.
[64]N.G. Leveson, J.L. Stolzy.Safety Analysis Using Petri Nets. IEEE Transactions on Software Engineering.1987. vol.13(3)386-397.
[65]Genrich H J. Predicate/Transition Nets:Lecture Notes in Computer Science. Berlin,1987. 207-247.
[66]Genrich H J, Hanisch H M, Wollhaf K. Verification of recipe-based control procedures of means of predicate/transition nets:Lecture Notes in Computer Science. Berlin,1994.278-297.
[67]Hanisch H.M. On the use of Petri nets for design, verification and optimization of control procedures for batch processes. IEEE International Conference on Systems, Man and Cybernetics. San Antonio,1994.326-330.
[68]Zuberek W M. Performance evaluation using unbound timed Petri nets. The Third International Workshop on Petri Nets and Performance Models. Kyoto, Japan,1989.180-186.
[69]Gerzson M., Csaki Z., Hangos K M. Qualitative model based verification of operating procedures by high level Petri nets. Computers& Chemical Engineering.1994, vol.18. S565-S569.
[70]Zimmermand A, Gunter H. A train control system case study in model-based real time system design:International parallel and distributed processing symposium (IPDPS). France,2003. 118-126.
[71]Andrea Bobbio, Giuliana Franceschinis, Rossano Gaeta, Luigi Portinale. Parametric Fault Tree for the Dependability Analysis of Redundant Systems and Its High-Level Petri Net Semantics. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, vol.29(3).
[72]D. C. Raiteri, G. Franceschinis, M. Iacono, and V. Vittorini.Repairable fault tree for the automatic evaluation of repairpolicies. In Proc. of the Performance and Dependability Symposium. Julv 2004.
[73]J. F. Meyer. Performability:a retrospective and some pointers to the future. Performance Evaluation.1992, vol.14(3&4).139-156.
[74]Gregor Gossler, Joseph Sifakis. Composition for Component-Based Modeling. In proceedings of FMCO'02. Leiden, Nederlands,2002.
[75]Daniel Duane Deavours. Formal Specification of the Mobius Modeling Framework[Dissertation]. University of Illinois at Urbana-Champaign,2001.
[76]F. Bause, P. Buchholz, P. Kemper. A toolbox for functional and quantitative analysis of DEDS. In Proc.10th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation. Lecture Notes in Computer Science 1469, Berlin:Springer-Verlag,1998.356-359.
[77]R.A. Sahner, K.S. Trivedi, A. Puliafito. Performance and Reliability Analysis of Computer Systems:An Example-based Approach Using the SHARPE Software Package. Kluwer Academic Publishers,1996.
[78]G. Ciardo, A. Miner. SMART:Simulation and Markovian Analyser for Reliability and Timing. In Proc.2nd International Computer Performance and Dependability Symposium (IPDS'96). IEEE Computer Society Press,1996.60.
[79]Lara, J. d., Vangheluwe. AToM3:A Tool for Multi-formalism and Meta-modelling. In Proceedings of the 5th international Conference on Fundamental Approaches To Software Engineering. R. Kutsche and H. Weber, Eds. Lecture Notes In Computer Science, vol.2306. London: Springer-Verlag,2002.174-188.
[80]V. Vittorini, M. Iacono, N. Mazzocca, G. Franceschinis, The OsMoSys approach to multiformalism modeling of systems. In Journal of Software and Systems Modeling, Volume 3, Issue 1, March 2004.68-81.
[81]H. Bohnenkamp, T. Courtney, D. Daly, S. Derisavi, H. Hermanns, J.-P. Katoen, R. Klaren, V. V. Lam, W. H. Sanders. On Integrating the Mobius and Modest Modeling Tools. In Proc. Int. Conf. on Dependable Systems and Networks. San Francisco, CA, June 22-25,2003.671.
[82]A. Bondavalli, M. Cin, D. Latella, A. Pataricza. High-level Integrated Design Environment for Dependability. In Proc. Fifth Int. Workshop on Object-Oriented Real-Time Dependable Systems (WORDS-99). Monterey, California, USA,1999.18-20.
[83]Ganesh J. Pai, Joanne Bechta Dugan. Automatic Synthesis of Dynamic Fault Trees from UML System Models. In Proc.13th International Symposium on Software Reliability Engineering (ISSRE'02).2002.243.
[84]Bernardi, S., Donatelli, S. Building Petri net scenarios for dependable automation systems. In Proc. of the 10th Int. Workshop on Petri nets and performance models (PNPM03). Urbana-Champaign, IL, USA,2003.72-81.
[85]W. S. Heath:Real-Time Software Techniques. Van Nostrand Reinhold, New York,1991.
[86]B. Jeng, E.J. Weyuker:Some Observations on Partition Testing. In Proceedings of the ACM SIGSOFT'89 Third Symposium on Software Testing, Analysis and Verification. Key West,1989.
[87]G. J. Myers. The Art of Software Testing. Wiley, New York,1979.
[88]T. Ostrand, M. Balcer. The Category-Partition Method for Specifying and Generating Functional Tests. Communications of the ACM.1988, vol.31(6).676-686.
[89]M. Grochtmann, K. Grimm. Classification-Trees for Partition Testing. Journal of Software Testing, Verification and Reliability.1993, vol.3(2).63-82.
[90]ANSI/IEEE Std 1012-1986. IEEE Standard for Software Verification and Validation Plans. The Institute of Electrical and Electronics Engineers, Inc., February 10,1987.
[91]G. Franceschinis, M. Gribaudo, M. lacono, N. Mazzocca, V. Vittorini. Towards an Object Based Multiformalism Multi-Solution Modeling Approach. In Proc. of the 2nd Workshop on Modelling of Objects, Components and Agents (MOCA02). Aarhus, DK,2002.
[92]Lyu M. R.软件可靠性工程手册.刘喜成译,北京：电子工业出版社,1997.
[93]陆民燕.软件可靠性增长测试的研究.航空学报,1995,vol.16(8).88-93.
[94]陈雪松,陆民燕,阮镰.软件可靠性测试数据生成方法研究.航空学报,2001,vol.22(6).510-512.
[95]David L. P., John A, Kwan S. P. Evaluation of Safety-critical software. Communication of ACM, 1990, vol.33(6).636-648.
[96]Parnas D L, Asmis G J K, Madey J. Assessment of safety-critical software in nuclear power plants. Nuclear Safety,1991, vol.32(2).189-198.
[97]Howden W E. good enough versus high assurance software testing and analysis methods. In: Regina S Sed. Proceedings of the Third IEEE International High-Assurance Systems Engineering Symposium[C]. Washington D C:IEEE Computer Society,1998.166-175.
[98]Miller W M, Morell L J, Noonan R E, et al. Estimating the probability of failure when testing reveals no failures. IEEE Trans On Software Engineering,1992, vol.18(1).33-34.
[99]Littlewood B, Strigini L. Assessment of ultra-high dependability for software-based systems. Communications of the ACM,1993, vol.36(11).69-80.
[100]Littlewood B, David W. Some conservative stopping rules for the operational testing of safety-critical software. IEEE Trans On Software Engineering,1997, vol.23(11).673-683.
[101]A. Denise, M. C. Gaudel, S. D. Gouraud. A Generate Method for Statistical Testing. Proceedings of the 15th International Symposium on Software Reliability Engineering.2004,25-34.
[102]D.Bird, C.Muoz. Automatic generation of random self cheching test cases. IBM Systems Journal,1983, vol22(2).229-265.
[103]J. Duran, S. Ntafos. An evaluation of random testing. IEEE Trans. On Software Engineering, 1986.638-666.
[104]Podgurski A, Marsri W, Mccleese Y. Estimate of Software Reliability by Stratified Sampleing. ACM Trans. On Software Engineering and Methodology,1999, vol.8(3).263-289.
[105]Statistical Software Testing Using Economic Exposure Assessments. Software Engineering Journal, September,1996.293-298.
[106]Karl R. P. H. Leung, Joseph K.Y, W. L. Yeung. Embedded Program Testing in Untestable Mobile Environment:An Experience of Trustworthiness Approach.11th Asia Pacific Software Engineering Conference.2006.630-637.
[107]Andre C. Coulter, Lockheed Martin. Graybox Software Testing Methodology Embedded Software Testing Technique. Proceedings of the 18th Digital Avionics Systems Conference. 1999.10.A.5-1-10.A.5-8.
[108]G.Bechker, L. Camarinopoulos. A Bayesian Estimation Method For The Failure Rate of A Possibly Correct Program. IEEE Trans on Software Engineering.1990, vol.16.1307-1310.
[109]K. N. Oikonomou. Prdictive with the dynamic Bayesian gamma mixture model. IEEE Trans on Systems, Man and Cybernetics, Part A,1997, vol.27.529-562.
[110]L. Pham, H. Pham. Software Reliability Models with time dependent hazard function based on Bayesian approach. IEEE Trans on Systems, Man and Cybernetics, Part A,2000, vol.30.25-35.
[111]Bojan Culic, Diwakar Chakravarthy. Bayesian framework for reliability assurance of a deployed safety critical system. IEEE,2000.321-329.
[112]Carol Smidts, Bojan Cukic Erdogan Gunel, Ming Li, et al. Software reliability corroboration. Proceeding of the 27th Annual NASA Goddard/IEEE Software Engineering Workshop.2003.
[113]Leveson N G. Safetware, system safety and computers. Addison Wesley,1995. [114] Budgen P J. Why risk analysis. IEE Colloquium on Risk Analysis Mehtods and Tools.1992. 1-4.
[115]Morries C. Hazard analysis using HAZOP:a case study. SAFECOMP 90.88-108.
[116]Finnie B W. Design for safety. IEE Colloquium on Safety Critical Software in Vehicle and Traffic Control,1990.1-4.
[117]Finnie B W. Introduction of new method for assuring safety into the software development process. IEE Colloquium on Safety Critical Software in Vehicle and Traffic Control,1990.1-2.
[118]Butler R W, Finelli G B. The infeasibility of quantifying the reliability of life-critical real-time software. IEEE Trans on Software Engineering,1993, vol.19(1).3-12.
[119]U. S. Nuclear Regulatory Commission. Fault Tree Handbook. NUREG-0492,1981.
[120]ENEA ISA-EUNET Presentation, http://tisgi.casaccia.enea.it/projects/isaeunet/SafetyCase /ppframe.htm.
[121]F.A.Patterson-Hine, Joanne Bechta Dugan. Modular Techniques for Dynamic Fault-tree Analysis. Proceedings Annual Reliability and Maintainability Symposium.1992.363-369.
[122]Astrium, Columbus:the European Space laboratory, http://www.astrium.eads.net/en/programme/columbus.html.
[122]Dijksta, E.W.:Notes on structured programming. T.H. Rep.70-WSK03(1970) http://www.sc.utexas.edu/user/EWD/ewdO2xx/EWD249.PDF 1,3
[123]Hetzel B. The complete guide to software testing.2nd edn, QED information sciences inc. 1988.
[124]Mayer G J. The art of software testing, John Wiley, New York,1979.
[125]Miller E F. Program testing:guest editor's introduction. IEEE Computer,1978, vol.11(4).10-12
[126]Fraser G, Wotawa F, Ammann P. Issues in using model checkers for test case generation[J]. J. Syst. Softw.,2009,82(9):1403-1418.
[127]Fraser G, Wotawa F. Test-case generation and coverage analysis for nondeterministic systems using model-checkers. Proceedings of the International Conference on Software Engineering Advances, Cap Esterel, French Riviera, France:IEEE Computer Society,2007:45-50.
[128]Belli F, Guldali B. A holistic approach to test-driven model checking. The 18th international conference on Innovations in Applied Artificial Intelligence, Bari, Italy:Springer-Verlag, 2005:321-331.
[129]ERTMS/ETCS SUBSET 076-5-2:Test cases related to features[EB/OL]. http://www.era.europa.eu/Core-Activities/ERTMS/Pages/ListOflnformativeSpecifications.aspx. PDF,2003.
[130]陈希孺.高等数理统计学.北京：清华大学出版社,1995.
[131]J.O. Berger. Statistical Decision Theory and Bayesian Analysis. New York:Sprinnger Verlag. 1985.
[132]中华人民共和国铁道部CTCS-3级列控系统系统标准规范系列------CTCS-3级列控系统系统需求规范(SRS).北京：中国铁道出版社,2009.
[133]UNISIG, ERTMS REGIONAL RAMS Requirements, Ref.06s0120.
[134]Chart, Vuong CT, Otp MR. An improved protocol test generation procedure based on UIOS. In: Landweber LH, ed. Symp. Proc. on Communications Architectures& Protocols. New York:ACM Press,1989.283-294.
[135]Abe AV, Dahbura AT, Lee D, Uyar MU. An optimization technique for protocol conformance test sequence generation based on UIO sequence and rural Chinese postman tour. IEEE Trans, on Communications.1991,vol.39(11).1604-1615.
[136]Sidhu DP, Leung T. Formal methods for protocol testing:A detailed study. IEEE Trans, on Software Engineering,1989,vol.15(4).413-426.
[137]Fujiwara S, Bochmarm GV. Test selection based on finite state models. IEEE Trans, on Software Engineering,1991,vol.17(6).591-603.
[138]Lamport L. The temporal logic of actions. ACM Trans, on Programming Language and Systems,1994,vol.16(3).872-923.
[139]AlurR, DillD. A theory of timed automata. Theoretical Computer Science,1994, vol.126(2).183-235.
[140]Rajeev Alur. Timed Automata. Computer-Aided Verification. LNCS 1633, London: Springer-Verlag.1999.8-22.
[141]Kaynar DK, Lynch N, Segala R, Vaandrager F. Timed I/O automata:A mathematical framework for modeling and analyzing real-time systems. In:Kaynar DK, Lyn ch N, Segala R, Vaandrager F, eds. Proc. of the 24th IEEE Real-Time Systems Symp. Washington:IEEE Computer Society,2003.166-177.
[142]Henzinger TA, Manna Z, Pnueli A. Timed transition system. In:Bakker JWD, Huizing C, Roever WPD, Rozenber8 G, eds. Proc. of the Real-Time:Theory in Practice, REX Workshop. LNCS 600, Berlin:Springer-Verlag,1992.226-251.
[143]Hessel, Anders, Larsen, Kim G, Mikucionis, Marius.Testing real-time systems using UPPAAL. Lecture Notes in Computer Science,2008.77-117.
[144]Bahareh Badban, Martin Franzle, Tino Teige. Test Automation for Hybrid Systems. Proceedings of the Third International Workshop on Software Quality Assurance.2006.14-21.
[145]T. Higashino, A. Nakata, K. Taniguchi, A. R. Cavalli. Generating test cases for a timed I/O automaton model. In G. Csopaki, S. Dibuz, and K. Tarnay, eds, Proc. IFIP Int'l Work. Test. Communicat. Syst. (IWTCS), Boston, MA:Kluwer Academic Publ,1999.197-214.
[146]KimYG, HongHS, BaeDH et al. Test cases generation from UML state diagram. IEEE Proceeding Software.1999, vol.146(4).187-192.
[147]Hong H S, Kim Y K, Cha S D et al. A test sequence selection method for reactive systems using statecharts. Software Testing Verification and Reliability.2000,vol.l0(4).203-227.
[148]Sidney Nogueira, Augusto Sampaio, Alexandre Mota. Guided Test Generation from CSP Models. Theoretical Aspects of Computing-ICTAC 2008, Lecture Notes in Computer Science, Springer-Verlag,2008.258-273.
[149]S. Helke, T. Neustupny, T. Santen. Automating Test Case Generation from Z Specifications with Isabelle. ZUM'97:The Z Formal Specification Notation, LNCS 1212, J.P. Bowen,M.G. Hinchey and D. Till, eds. Springer-Verlag,1997.52-71.
[150]R.M. Hierons, M. Harman, H. Singh,2003. Automatically generating information from a Z specification to support the Classification Tree Method.3rd International Conference of B and Z Users, June 4-6,2003, vol.2651.388-407.
[151]R. M. Hierons, S. Sadeghipour, H. Singh, Testing a System specified using Statecharts and Z. Information and Software Technology.2001, vol.43(2).137-149.
[152]R.M. Hierons. Testing from a Z specification. The Journal of Software Testing, Verification, and Reliability,1997, vol.7(1).19-33.
[153]P.G. Bishop and R.E. Bloomfield, "A Conservative Theory for Long-Term Reliability Growth"Prediction. IEEE Trans. Reliability, vol.45, no.4, Dec.96, pp.550-560, ISSN 0018-9529
[154]P.G. Bishop and R.E. Bloomfield, "Worst Case Reliability Prediction Based on a Prior Estimateof Residual Defects", Thirteenth International Symposium on Software Reliability Engineering(ISSRE'02), pp.295-303, November 12-15, Annapolis, Maryland, USA,2002
[155]D.M. Yellin, R.E. Strom. Protocol Specifications and Component Adaptors. ACM Transactions on Programming Languages and Systems,1997, vol.19(2).
[156]季学胜,唐涛CTCS-3级列车运行控制系统综合测试平台研究.铁道通信信号,2007,43(7).1-3.
[157]张曙光CTCS-3级列控系统总体技术方案.北京：中国铁道出版社,2008.