基于通信的列车控制系统可信构造:形式化方法综述
|
摘要
基于通信的列车控制系统(communication based train control system,简称CBTC)已经成为世界范围内建造轨道交通信号系统的标准制式.CBTC采用更加灵活和精确的列车控制,并提供连续的安全列车间隔保证和超速防护,在很大程度上提高了轨道交通运输的效率和安全性.尽管CBTC能够精确地实施实时控制,但由于CBTC涉及计算、通信与控制这3个方面的实时协同,系统设计与实现异常复杂.由设计缺陷而导致严重的灾难、事故和损失屡见不鲜.作为一个典型的安全攸关系统,如何保证CBTC的可信构造已成为领域研发人员关注的焦点与面临的最大挑战.鉴于在软硬件领域的成功经验,形式化方法目前已被公认为是保障CBTC可信性的一种有效方案.围绕CBTC的可信构造,从其生命周期的3个重要阶段,即系统需求分析、设计建模与底层实现入手,针对CBTC在可信方面的典型特征,梳理分析了CBTC系统在可信构造方面面临的挑战、国内外研究现状和发展趋势,全面介绍了形式化方法在CBTC可信构造中扮演的角色.
Communication-based train control system(CBTC) has become the mainstream infrastructure for the railway signal systems around the world. Unlike traditional track circuit-based railway control systems, CBTC adopts a more flexible and accurate control mechanism to provide uninterrupted services to enable guarantee safeguard between adjacent trains and protection for over-speeding. Therefore, CBTC significantly improves the efficiency and safety of train-based transportation. Although CBTC can accurately conduct real-time control, its design and implementation are extremely complex due to the integration of heterogeneous computation, communication and control components. Consequently, breakdowns caused by CBTC design flaws are inevitable. Therefore, how to guarantee the trustworthiness of CBTC, as for any typical safety-critical system, becomes a big challenge for researchers and practitioners. Due to the huge success in both hardware and software domains, formal methods are now considered as a promising means for trustworthy construction of CBTC systems. This article surveys the three most important stages during the trustworthy construction of CBTC systems, i.e., requirement analysis, design modeling, and bottom-level implementation. It not only comprehensively presents the important roles of the state-of-the-art formal methods and tools during the trustworthy CBTC construction, but also introduces the development trends as well as technical challenges for future CBTC.
Communication-based train control system(CBTC) has become the mainstream infrastructure for the railway signal systems around the world. Unlike traditional track circuit-based railway control systems, CBTC adopts a more flexible and accurate control mechanism to provide uninterrupted services to enable guarantee safeguard between adjacent trains and protection for over-speeding. Therefore, CBTC significantly improves the efficiency and safety of train-based transportation. Although CBTC can accurately conduct real-time control, its design and implementation are extremely complex due to the integration of heterogeneous computation, communication and control components. Consequently, breakdowns caused by CBTC design flaws are inevitable. Therefore, how to guarantee the trustworthiness of CBTC, as for any typical safety-critical system, becomes a big challenge for researchers and practitioners. Due to the huge success in both hardware and software domains, formal methods are now considered as a promising means for trustworthy construction of CBTC systems. This article surveys the three most important stages during the trustworthy construction of CBTC systems, i.e., requirement analysis, design modeling, and bottom-level implementation. It not only comprehensively presents the important roles of the state-of-the-art formal methods and tools during the trustworthy CBTC construction, but also introduces the development trends as well as technical challenges for future CBTC.
引文
[1]Gao CH.Research on the key techniques of the independent and innovative CBTC.Modern Urban Transit,2011,24(4):1-4(in Chinese with English abstract).
[2]European Committee for Electrotechnical Standardization.EN50128,Railway Applications?Software for Railway Control and Protection Systems.Brussels:CENELEC,1997.
[3]Cao Y,Tang T,Xu TH,Mu JC.Application of formal methods in train control system.Journal of Traffic and Transportation Engineering,2010,10(1):112-126(in Chinese with English abstract).
[4]Tang T,Zhao LB.Train Control System Design and Verification Methods Based on Model.Beijing:China Railway Publishing House,2014(in Chinese).
[5]Fantechi A.Twenty-Five years of formal methods and railways:what next.In:Proc.of the Int’l Conf.on Software Engineering and Formal Methods.Springer Int’l Publishing,2013.167-183.[doi:10.1007/978-3-319-05032-4_13]
[6]IEEE Std 1850-2010.IEEE Standard for Property Specification Language(PSL).2010.1-182.
[7]Hu XL.Modeling and verification of level transition scene in CTCS-3 level train control system based on UML and UPPAAL[MS.Thesis].Lanzhou:Lanzhou Jiaotong University,2015(in Chinese with English abstract).
[8]Liu JT,Tang T,Xiu TH,Zhao L.Formal verification of CTCS-3 system requirements specification based UML model.China Railway Science,2011,32(3):93-99(in Chinese with English abstract).
[9]Chiappini A,Cimatti A,Macchi L,Rebollo O,Roveri M,Susi A,Vittorini B.Formalization and validation of a subset of the European train control system.In:Proc.of the Int’l Conf.on Software Engineering.2010.109-118.[doi:10.1145/1810295.1810312]
[10]Zhang QX.Research on the method of verification of train control system requirements specification based on x UML[MS.Thesis].Beijing:Beijing Jiaotong University,2011(in Chinese with English abstract).
[11]Bloem R,Cimatti A,Greimel K,Hofferek G,K?nighofer R,Roveri M,Seeber R.RATSY?A new requirements analysis tool with synthesis.In:Proc.of the Int’l Conf.on Computer Aided Verification(CAV).Berlin:Springer-Verlag,2010.425-429.[doi:10.1007/978-3-642-14295-6_37]
[12]He LY,Zhao L,Chen RJ.Property-Driven modeling and verification for requirements of train control system.Railway Computer Application,2014,(2):1-6(in Chinese with English abstract).
[13]Chen RJ,Zhao L,He LY.UML-Based requirements analysis methods and attributes used in the train control system requirements specification.Railway Signaling&Communication,2013,(2):80-84(in Chinese with English abstract).
[14]Zhao L,Tang T,Cheng RJ,He LY.Property based requirements analysis for train control system.Journal of Computational Information Systems,2013,9(3):915-922.
[15]Sommerville I,Sawyer P.Requirements Engineering.Wiley Publishing,1998.
[16]Yuan L,Tang T,Li K.Modelling and verification of the system requirement specification of train control system using SDL.In:Proc.of the Int’l Symp.on Autonomous Decentralized Systems.2011.81-85.[doi:10.1109/ISADS.2011.17]
[17]Issad M,Koul L,Rauzy A.A contribution to safety analysis of railway CBTC systems using Scola.In:Safety and Reliability of Complex Engineered Systems.CRC Press,2015.459-467.[doi:10.1201/b19094-64]
[18]Faber J,Jacobs S,Sofronie-Stokkermans V.Verifying CSP-OZ-DC specifications with complex data types and timing parameters.In:Proc.of the Int’l Conf.on Integrated Formal Methods.Berlin:Springer-Verlag,2007.233-252.[doi:10.1007/978-3-540-73210-5_13]
[19]Abo R,Voisin L.Formal implementation of data validation for railway safety-related systems with OVADO.In:Proc.of the SEFN Workshops.Springer Int’l Publishing,2014.221-236.[doi:10.1007/978-3-319-05032-4_17]
[20]Abrial JR.Modeling in Event-B:System and Software Engineering.Cambridge University Press,2010.
[21]Milner R.A Calculus of Communicating Systems.New York:Springer-Verlag,1980.[doi:10.1007/3-540-10235-3]
[22]Hoare CAR.Communicating Sequential Processes.Englewood Cliffs:Prentice Hall Int’l,1985.
[23]Zou L,LüJD,Wang SL,Zhan NJ,Tang T,Yuan L,Liu Y.Verifying Chinese train control system under a combined scenario by theorem proving.In:Proc.of the Int’l Verified Software:Theories,Tools,and Experiments.Berlin:Springer-Verlag,2013.262-280.[doi:10.1007/978-3-642-54108-7_14]
[24]Pohl K.Requirements Engieering:Fundamentals,Principles,and Techniques.Springer-Verlag,2010.
[25]Liu JT,Tang T,Xiu TH,Zhao L.Formal verification of CTCS-3 system requirements specification based UML model.China Railway Science,2011,32(3):93-99(in Chinese with English abstract).
[26]Ahmad E,Dong YW,Larson B,Lu J,Tang T,Zhan NJ.Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL.Science China Information Sciences,2015,58(11):1-20(in Chinese with English abstract).
[27]Andre C,Mallet F,Simone RD.Modeling time(s).In:Proc.of the Int’l Conf.on Model Driven Engineering Languages and Systems(Mo DELS).Berlin:Springer-Verlag,2007.559-573.[doi:10.1007/978-3-540-75209-7_38]
[28]Alur R,Dill D.A theory of timed automata.Theoretical Computer Science,1994,126(2):183-235.[doi:10.1016/0304-3975(94)90010-8]
[29]Zhou CC,Hoare CA,Ravn AP.A calculus of duration.Information Processing Letters,1991,40(5):269-276.[doi:10.1016/0020-0190(91)90122-X]
[30]UML Tools.2016.https://www.wikiwand.com/en/List_of_Unified_Modeling_Language_tools
[31]IBM Rational Software.2016.https://www.ibm.com/software/rational
[32]SAP Power Designer.2016.http://go.sap.com/product/data-mgmt/powerdesigner-data-modeling-tools.html
[33]Pragma Dev Studio.2016.http://www.pragmadev.com/
[34]IBM SDL Suite.2016.http://www-01.ibm.com/software/awdtools/sdlsuite/
[35]PAT Model Checker.2016.http://www.patroot.com/
[36]Aceituna D,Do H,Lee SW.SQ2E:An approach to requirements validation with scenario question.In:Proc.of the Int’l Conf.on Asia Pacific Software Engineering.2010.33-42.[doi:10.1109/APSEC.2010.14]
[37]Aceituna D,Do H,Lee SW.Interactive requirements validation for reactive systems through virtual requirements prototype.In:Proc.of the Int’l Conf.on Model-Driven Requirements Engineering Workshop(Mo DRE).2011.1-10.[doi:10.1109/Mo DRE.2011.6045361]
[38]Lee YK,In HP,Kazman R.Customer requirements validation method based on mental models.In:Proc.of the Int’l Conf.on Asia-Pacific Software Engineering Conf.2014.199-206.[doi:10.1109/APSEC.2014.39]
[39]IBM Rational Requisite Pro.http://open-services.net/software/ibm-rational-requisite-pro/
[40]The Pro B Animator and Model Checker.https://www3.hhu.de/stups/prob/
[41]UPPAAL.http://www.uppaal.org/
[42]Maio WK,Pu GG,Yao YB,Su T,Bao DZ,Liu Y.Automated requirements validation for ATP software via specification review and testing.In:Proc.of the Int’l Conf.on Formal Engineering Methods(ICFEM).Springer Int’l Publishing,2016.26-40.[doi:10.1007/978-3-319-47846-3_3]
[43]Frehse G.PHAVer:Algorithmic verification of hybrid systems past Hy Tech.Int’l Journal on Software Tools for Technology Transfer(STTT),2008,10(3):263-279.[doi:10.1007/s10009-007-0062-x]
[44]Podelski A,Rybalchenko A.Transition predicate abstraction and fair termination.ACM SIGPLAN Notices,2005,40(1):132-144.[doi:10.1145/1047659.1040317]
[45]Podelski A,Rybalchenko A.ARMC:The logical choice for software model checking with abstraction refinement.In:Practical Aspects of Declarative Languages.Berlin:Springer-Verlag,2007.245-259.[doi:10.1007/978-3-540-69611-7_16]
[46]Olderog ER.Automatic verification of combined specifications:An overview.Electronic Notes in Theoretical Computer Science,2008,207:3-16.[doi:10.1016/j.entcs.2008.03.082]
[47]Cho C,Choi D,Quan Z,Choi S,Park G,Ryou M.Modeling of CBTC carborne ATO functions using SCADE.In:Proc.of the Int’l Conf.on Control,Automation and Systems.2011.1089-1093.
[48]Simulink.2016.https://www.mathworks.com/products/simulink
[49]Feiler PH,Gluch DP,Hudak JJ.The architecture analysis&design language(AADL):An introduction.Technical Report,CMU/SEI-2006-TN-011,Carnegie Mellon University,2006.
[50]OSATE2.2016.http://osate.github.io/
[51]Li C,Zhang L.Train control system modeling and design based on AADL.In:Proc.of the Int’l Conf.on Software Engineering and Service Science.2015.474-477.[doi:10.1109/ICSESS.2015.7339100]
[52]Ahmad E,Dong YW,Larson B,LüJ,Tang T,Zhan NJ.Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL.Science China Information Sciences,2015,58(11):1-20.[doi:10.1007/s11432-015-5346-2]
[53]Yang CS,Lim JL,Um JK,Han JM,Bang Y,Kim HH,Yun YH,Kim CJ,Cho YJ.Developing CBTC software using model-driven development approach.In:Proc.of the WCRR.2008.
[54]Yang SW.Modeling and safety verification of zone controller in CBTC with UML[MS.Thesis].Beijing:Beijing Jiaotong University,2008(in Chinese with English abstract).
[55]Henzinger TA.The theory of hybrid automata.In:Proc.of the IEEE Symp.on Logic in Computer Science.Berlin:Springer-Verlag,1996.278-292.[doi:10.1007/978-3-642-59615-5_13]
[56]Bu L,Wang Q,Chen X,Wang L,Zhang T,Zhao J,Li X.Toward online hybrid systems model checking of cyber-physical systems’time-bounded short-run behavior.ACM SIGBED Review,2011,8(2):7-10.[doi:10.1145/2000367.2000368]
[57]LüJD,Tang T,Yan F,Xu TH.UPPAAL-Based simulation and verification of CBTC zone control subsystem in rail transportation.Journal of the China Railway Society,2009,31(3):59-64(in Chinese with English abstract).
[58]SCADE Suite.2016.http://www.esterel-technologies.com/products/scade-suite/
[59]Ren X,Zhou MC.Tactical scheduling of rail operations:A Petri net approach.In:Proc.of the Int’l Conf.on Intelligent Systems for the 21st Century.1995.3087-3092.[doi:10.1109/ICSMC.1995.538256]
[60]Hei X,Takahashi S,Nakamura H.Distributed interlocking system and its safety verification.In:Proc.of the Int’l Conf.on Intelligent Control and Automation.2006.8612-8615.[doi:10.1109/WCICA.2006.1713661]
[61]H?rste MM,Schnieder E.Modelling and simulation of train control systems using Petri nets.In:Proc.of the World Congress on Formal Methods.Berlin:Springer-Verlag,1999.1867-1867.[doi:10.1007/3-540-48118-4_58]
[62]Ren GB.Modelling and analysis of high-speed train tracking process based on high-level Petri net.[Ph.D.Thesis].Lanzhou:Lanzhou Jiaotong University,2015(in Chinese with English abstract).
[63]Boudi Z,Collart-Dutilleul S,Khaddour M.High level Petri net modeling for railway safety critical scenarios.In:Proc.of the Int’l Conf.on Formal Methods for Automation and Safety in Railway and Automotive Systems.2014.65-75.
[64]CPN Tool.2016.http://cpntools.org/
[65]Wu DY,Zhang Y.Researching colored Petri nets model of communication based train control system.Journal of System Simulation,2005,17(10):2388-2391(in Chinese with English abstract).
[66]Zhao SX,Wang XL.Movement authority process formal modeling for China train control system-3.Computer Engineering and Design,2013,34(6):2119-2124.
[67]Ahmad E,Dong YW,Larson B,LüJ,Tang T,Zhan NJ.Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL.Science China Information Sciences,2015,58(11):1-20.[doi:10.1007/s11432-015-5346-2]
[68]Sun P,Collart-Dutilleul S,Bon P.A formal modeling methodology of french railway interlocking system via HCPN.WIT Trans.on the Built Environment.2014,135:1-10.[doi:10.2495/CR140711]
[69]Zimmermann A,Hommel G.Towards modeling and evaluation of ETCS real-time communication and operation.Journal of Systems and Software,2005,77(1):47-54.[doi:10.1016/j.jss.2003.12.039]
[70]Zhou G,Zhao HB.Modeling and safety analysis of track occupancy checking logic in section signaling.Journal of the China Railway Society,2016,38(4):66-73(in Chinese with English abstract).
[71]Zhou G,Zhao H.Modeling and quantitative safety analysis of Chinese train control system of systems.In:Proc.of the Int’l Conf.on Intelligent Transportation Systems(ITSC).2015.381-386.[doi:10.1109/ITSC.2015.71]
[72]Rigorous Approach to Industrial Software Engineering.2016.http://spd-web.terma.com/Projects/RAISE/
[73]Haxthausen AE,Peleska J.Formal development and verification of a distributed railway control system.IEEE Trans.on Software Engineering,2000,26(8):687-701.[doi:10.1109/32.879808]
[74]Xu SZ.Modeling and analysis of RBC handover based on timed RAISE[Ph.D.Thesis].Lanzhou:Lanzhou Jiaotong University,2015(in Chinese with English abstract).
[75]PLASMA Lab.2016.https://project.inria.fr/plasma-lab/
[76]Modelica.2016.https://www.modelica.org/
[77]CHARON.2016.https://rtg.cis.upenn.edu/mobies/charon/
[78]Nu SMV.2016.http://nusmv.fbk.eu/
[79]The Coq Proof Assistant.2016.https://coq.inria.fr/
[80]Rodin.2016.http://www.event-b.org/
[81]Probabilistic Symbolic Model Checker.2016.http://www.prismmodelchecker.org
[82]Goodman CJ,Siu LK,Ho TK.A review of simulation models for railway systems.In:Proc.of the Int’l Conf.on Developments in Mass Transit Systems.1998.80-85.[doi:10.1049/cp:19980101]
[83]Cimatti A,Corvino R,Lazzaro A,Narasamdya I,Rizzo T,Roveri M,Tchaltsev A.Formal verification and validation of ERTMS industrial railway train spacing system.In:Proc.of the Int’l Conf.on Computer Aided Verification.Berlin:Springer-Verlag,2012.378-393.[doi:10.1007/978-3-642-31424-7_29]
[84]Hemmat MHA,Mohamed OA,Boukadoum M.Formal modeling,verification and implementation of a train control system.In:Proc.of the Int’l Conf.on Microelectronics(ICM).2015.134-137.[doi:10.1109/ICM.2015.7438006]
[85]Qian J,Liu J,Chen XH,Sun JF.Modeling and verification of zone controller:The SCADE experience in china's railway systems.In:Proc.of the Int’l Workshop on Complex Faults and Failures in Large Software Systems.2015.48-54.[doi:10.1109/COUFLE SS.2015.15]
[86]Platzer A.Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics.Berlin:Springer-Verlag,2010.[doi:10.1007/978-3-642-14509-4]
[87]Zou L,Zhan NJ,Wang SL,Fr?nzle M,Qin SC.Verifying simulink diagrams via a hybrid Hoare logic prover.In:Proc.of the Int’l Conf.on Embedded Software,Vol.9.2013.1-10.[doi:10.1109/EMSOFT.2013.6658587]
[88]Zhou X,Zhang Y.Security analysis about a train control center based on a Bayesian network.In:Proc.of the Int’l Conf.on Transportation Engineering.Reston:American Society of Civil Engineers.2015.
[89]Xu TH,Tang T,Gao CH,Cai BG.Dependability analysis of the data communication system in train control system.Science in China Series E:Technological Sciences,2009,52(9):2605-2618.[doi:10.1007/s11431-009-0183-4]
[90]Zhao HL,Xu TH,Tang T.Towards modeling and evaluation of availability of communication based train control(CBTC)system.In:Proc.of the Int’l Conf.on Communication Technology and Applications.2009.860-863.[doi:10.1109/ICCOMTA.2009.5349076]
[91]Bu L,Wang Q,Chen X,Wang L,Zhang T,Zhao J,Li X.Toward online hybrid systems model checking of cyber-physical systems’time-bounded short-run behavior.ACM SIGBED Review,2011,8(2):7-10.[doi:10.1145/2000367.2000368]
[92]LüJD,Tang T,Yan F,Xu TH.UPPAAL-Based simulation and verification of CBTC zone control subsystem in rail transportation.Journal of the China Railway Society,2009,31(3):59-64(in Chinese with English abstract).
[93]David A,Du D,Larsen KG,Legay A,Miku?ionis M.Optimizing control strategy using statistical model checking.In:Proc.of the NASA Formal Methods Symp.Berlin:Springer-Verlag,2013.352-367.[doi:10.1007/978-3-642-38088-4_24]
[94]Gu F,Zhang XQ,Chen MS,Grosse D,Drechsler R.Quantitative timing analysis of UML activity diagrams using statistical model checking.In:Proc.of the Int’l Conf.on Design,Automation&Test in Europe Conf.&Exhibition(DATE).2016.780-785.[doi:10.3850/9783981537079_0339]
[95]Mc Dermid J,Kelly T.Software in safety critical systems-achievement and prediction.Nuclear Future,2006,(2):140-146.[doi:10.1680/nuen.2006.2.3.140]
[96]Ellims M.On wheels,nuts and software.In:Proc.of the Australian Workshop on Safety Critical Systemsand Software.Parlinghurst:Austranlian Computer Society,2004.67-76.
[97]Heimdahl MPE.Safety and software intensive systems:Challenges old and new.In:Proc.of the Future of Software Engineering.2007.137-152.[doi:10.1109/FOSE.2007.18]
[98]Lutz RR.Software engineering for safety:A roadmap.In:Proc.of the Future of Software Engineering.New York:ACM,2000.213-226.[doi:10.1145/336512.336556]
[99]Leea JH,Hwanga JG,Shina D,Leea KM,Kimb SU.Development of verification and conformance testing tools for a railway signaling communication protocol.Computer Standards and Interfaces,2009,31(2):362-371.[doi:10.1016/j.csi.2008.05.011]
[100]Didrich K,Herbs S,Vieria M.Applying model-based testing to a train control system.In:Proc.of the INFORMATIK.2006.249-256.
[101]Zhang Y.Fault related formal test method of the software in train control system[Ph.D Thesis].Beijing:Beijing Jiaotong University,2012(in Chinese with English abstract).
[102]UPPAAL-TRON.2016.http://people.cs.aau.dk/~marius/tron/
[103]UPPAAL Cover.http://www.hessel.nu/Co Ver/
[104]Hessel A,Larsen KG,Mikucionis M,Nielsen B,Pettersson P,Skou A.Testing real-time systems using UPPAAL.In:Proc.of the Formal Methods and Testing.2008.77-117.[doi:10.1007/978-3-540-78917-8_3]
[105]LüJD,Zhu XL,Wang HF,Li KC,TANG T.Research on conformance testing for nondeterministic delay in high speed train control system based on UPPAAL-TRON.Journal of the China Railway Society,2016,38(1):54-64(in Chinese with English abstract).
[106]LüJD,Ren PC,Lei C,Li KC,Tang T.Model-Based test case generation for function testing of CTCS-3 onboard subsystem.Journal of Control and Automation,2015,8(1):171-178.[doi:10.14257/ijca.2015.8.10.17]
[107]Yang L,LüJD,L Y,Li CL,Zhao WH.Research on model-based test case generation method of onboard subsystem in CTCS-3.Journal of the China Railway Society,2014,36(8):55-62(in Chinese with English abstract).
[108]Chen X,Jang P,Zhang YF,Huang C,Zhou Y.Method of automatic test case generation for safety-critical scenarios in train control systems.Ruan Jian Xue Bao/Journal of Software,2015,26(2):269-278(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/4780.htm[doi:10.13328/j.cnki.jos.004780]
[109]Yin YF,Liu B,Ni HY.Real-Time embedded software testing method based on extended finite state machine.Journal of Systems Engineering and Electronics,2012,23(2):276-285.[doi:10.1109/JSEE.2012.00035]
[110]Hilken C,Hübner F,Peleska J.Combination of behavioral and parametric diagrams for model-based testing.Technical Report,open ECTS Report 2014-11-25,University of Bremen,2015.
[111]Ministry of Railway of the People’s Republic of China.TB/T 2615-1994 Railway Signal Failure—Safety Principles.Beijing:China Railway Publishing House,1995(in Chinese).
[112]Morell LJ.A theory of fault-based testing.IEEE Trans.on Software Engineering,1990,16(8):844-857.[doi:10.1109/32.57623]
[113]Tu HY,Wu FM.Embedding fault in simulation environment for software black-box testing.Ruan Jian Xue Bao/Journal of Software,1998,10(5):516-520(in Chinese with English abstract).
[114]Gay G,Staats M,Whalen M,Heimdahl M.The risks of coverage-directed test case generation.IEEE Trans.on Software Engineering,2015,41(8):803-819.[doi:10.1109/TSE.2015.2421011]
[115]Baker R,Habli I.An empirical evaluation of mutation testing for improving the test quality of safety-critical software.IEEE Trans.on Software Engineering,2013,39(6):787-805.[doi:10.1109/TSE.2012.56]
[116]Sun HY,Chen MS,Zhang M,Liu J,Zhang Y.Improving defect detection ability of derived test cases based on mutated UML activity diagrams.In:Proc.of the Annual Computer Software and Applications Conf.2016.275-280.[doi:10.1109/COMPSAC.2016.136]
[117]Li T,Li KC,Lv JD,Yuan L,Fu Q,Wen T.Mutation testing for evaluating the completeness of test cases in high-speed train control system.In:Proc.of the Int’l Conf.on Intelligent Transportation Systems.2015.777-782.[doi:10.1109/ITSC.2015.131]
[118]Wang X,Ma LC,Tang T.Study on formal modeling andverification of safety computer platform.Advances in Mechanical Engineering,2016,8(5):1-13.[doi:10.1177/1687814016649115]
[119]Lu QJ.Modeling and analysis of CBTC onboard equipment based on colored Petri net[MS.Thesis].Beijing:Beijing Jiaotong University,2008(in Chinese with English abstract).
[120]Zhu L,Ning B.The design of the CBTC train-ground communication system based on IEEE 802.11g standard.China Railway Science,2010,31(5):119-124(in Chinese with English abstract).
[1]郜春海.自主创新CBTC系统的核心技术研究.都市快轨交通,2011,24(4):1-4.
[3]曹源,唐涛,徐田华,穆建成.形式化方法在列车运行控制系统中的应用.交通运输工程学报,2010,10(1):112-126.
[4]唐涛,赵林编.基于模型的列车运行控制系统设计与验证方法.北京:中国铁道出版社,2014.
[7]胡雪莲.基于UML和UPPAAL的CTCS-3级列控系统等级转换场景建模与验证[硕士学位论文].兰州:兰州交通大学,2015.
[8]刘金涛,唐涛,徐田华,赵林.基于UML的CTCS-3级列控系统需求规范形式化验证方法.中国铁道科学,2011,32(3):93-99.
[10]张庆新.基于x UML的列控系统需求规范验证方法研究[硕士学位论文].北京:北京交通大学,2011.
[12]何丽芸,赵林,程瑞军.属性驱动的列车控制系统需求建模与验证.铁路计算机应用,2014,(2):1-6.
[13]程瑞军,赵林,何丽芸.基于UML及属性的需求分析方法在列控系统需求规范中的应用.铁道通信信号,2013,(2):80-84.
[25]刘金涛.基于STPA的需求阶段的高速列车运行控制系统安全分析方法研究[博士学位论文].北京:北京交通大学,2015.
[54]杨旭文.基于UML的CBTC系统区域控制器的建模与安全性验证[硕士学位论文].北京:北京交通大学,2008.
[57]吕继东,唐涛,燕飞,徐天华.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证.铁道学报,2009,31(3):59-64.
[62]任国彬.基于高级Petri网的高速列车追踪运行过程建模与分析[硕士学位论文].兰州:兰州交通大学,2015.
[65]吴东勇,张勇.基于通信的列车控制系统的有色Petri网模型的研究.系统仿真学报,2005,17(10):2388-2391.
[70]周果,赵会兵.区间占用检查逻辑的建模与安全分析.铁道学报,2016,38(4):66-73.
[74]徐世泽.基于Timed RAISE的RBC切换建模与分析[硕士学位论文].兰州:兰州交通大学,2015.
[101]张岩.列车运行控制系统软件故障相关形式化测试方法[博士学位论文].北京:北京交通大学,2012.
[105]吕继东,朱晓琳,王海峰,李开成,唐涛.基于UPPAAL-TRON的高速铁路列控系统非确定性时延一致性测试研究.铁道学报,2016,38(1):54-64.
[107]袁磊,吕继东,刘雨,李辰岭,赵伟慧.一种全覆盖的列控车载系统测试用例自动生成算法研究.铁道学报,2014,36(8):55-62.
[108]陈鑫,姜鹏,张一帆,黄超,周岩.一种面向列车控制系统中安全攸关场景的测试用例自动生成方法.软件学报,2015,26(2):269-278.http://www.jos.org.cn/1000-9825/4780.htm[doi:10.13328/j.cnki.jos.004780]
[111]中华人民共和国铁道部.TB/T 2615-1994铁道信号故障——安全原则.北京:中国铁道出版社,1995.
[119]陆启进.基于有色Petri网的CBTC车载设备应用软件的建模与分析[硕士学位论文].北京:北京交通大学,2008.
[120]朱力,宁滨.基于IEEE 802.11g标准的CBTC车地通信系统设计.中国铁道科学,2010,31(5):119-124.
[2]European Committee for Electrotechnical Standardization.EN50128,Railway Applications?Software for Railway Control and Protection Systems.Brussels:CENELEC,1997.
[3]Cao Y,Tang T,Xu TH,Mu JC.Application of formal methods in train control system.Journal of Traffic and Transportation Engineering,2010,10(1):112-126(in Chinese with English abstract).
[4]Tang T,Zhao LB.Train Control System Design and Verification Methods Based on Model.Beijing:China Railway Publishing House,2014(in Chinese).
[5]Fantechi A.Twenty-Five years of formal methods and railways:what next.In:Proc.of the Int’l Conf.on Software Engineering and Formal Methods.Springer Int’l Publishing,2013.167-183.[doi:10.1007/978-3-319-05032-4_13]
[6]IEEE Std 1850-2010.IEEE Standard for Property Specification Language(PSL).2010.1-182.
[7]Hu XL.Modeling and verification of level transition scene in CTCS-3 level train control system based on UML and UPPAAL[MS.Thesis].Lanzhou:Lanzhou Jiaotong University,2015(in Chinese with English abstract).
[8]Liu JT,Tang T,Xiu TH,Zhao L.Formal verification of CTCS-3 system requirements specification based UML model.China Railway Science,2011,32(3):93-99(in Chinese with English abstract).
[9]Chiappini A,Cimatti A,Macchi L,Rebollo O,Roveri M,Susi A,Vittorini B.Formalization and validation of a subset of the European train control system.In:Proc.of the Int’l Conf.on Software Engineering.2010.109-118.[doi:10.1145/1810295.1810312]
[10]Zhang QX.Research on the method of verification of train control system requirements specification based on x UML[MS.Thesis].Beijing:Beijing Jiaotong University,2011(in Chinese with English abstract).
[11]Bloem R,Cimatti A,Greimel K,Hofferek G,K?nighofer R,Roveri M,Seeber R.RATSY?A new requirements analysis tool with synthesis.In:Proc.of the Int’l Conf.on Computer Aided Verification(CAV).Berlin:Springer-Verlag,2010.425-429.[doi:10.1007/978-3-642-14295-6_37]
[12]He LY,Zhao L,Chen RJ.Property-Driven modeling and verification for requirements of train control system.Railway Computer Application,2014,(2):1-6(in Chinese with English abstract).
[13]Chen RJ,Zhao L,He LY.UML-Based requirements analysis methods and attributes used in the train control system requirements specification.Railway Signaling&Communication,2013,(2):80-84(in Chinese with English abstract).
[14]Zhao L,Tang T,Cheng RJ,He LY.Property based requirements analysis for train control system.Journal of Computational Information Systems,2013,9(3):915-922.
[15]Sommerville I,Sawyer P.Requirements Engineering.Wiley Publishing,1998.
[16]Yuan L,Tang T,Li K.Modelling and verification of the system requirement specification of train control system using SDL.In:Proc.of the Int’l Symp.on Autonomous Decentralized Systems.2011.81-85.[doi:10.1109/ISADS.2011.17]
[17]Issad M,Koul L,Rauzy A.A contribution to safety analysis of railway CBTC systems using Scola.In:Safety and Reliability of Complex Engineered Systems.CRC Press,2015.459-467.[doi:10.1201/b19094-64]
[18]Faber J,Jacobs S,Sofronie-Stokkermans V.Verifying CSP-OZ-DC specifications with complex data types and timing parameters.In:Proc.of the Int’l Conf.on Integrated Formal Methods.Berlin:Springer-Verlag,2007.233-252.[doi:10.1007/978-3-540-73210-5_13]
[19]Abo R,Voisin L.Formal implementation of data validation for railway safety-related systems with OVADO.In:Proc.of the SEFN Workshops.Springer Int’l Publishing,2014.221-236.[doi:10.1007/978-3-319-05032-4_17]
[20]Abrial JR.Modeling in Event-B:System and Software Engineering.Cambridge University Press,2010.
[21]Milner R.A Calculus of Communicating Systems.New York:Springer-Verlag,1980.[doi:10.1007/3-540-10235-3]
[22]Hoare CAR.Communicating Sequential Processes.Englewood Cliffs:Prentice Hall Int’l,1985.
[23]Zou L,LüJD,Wang SL,Zhan NJ,Tang T,Yuan L,Liu Y.Verifying Chinese train control system under a combined scenario by theorem proving.In:Proc.of the Int’l Verified Software:Theories,Tools,and Experiments.Berlin:Springer-Verlag,2013.262-280.[doi:10.1007/978-3-642-54108-7_14]
[24]Pohl K.Requirements Engieering:Fundamentals,Principles,and Techniques.Springer-Verlag,2010.
[25]Liu JT,Tang T,Xiu TH,Zhao L.Formal verification of CTCS-3 system requirements specification based UML model.China Railway Science,2011,32(3):93-99(in Chinese with English abstract).
[26]Ahmad E,Dong YW,Larson B,Lu J,Tang T,Zhan NJ.Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL.Science China Information Sciences,2015,58(11):1-20(in Chinese with English abstract).
[27]Andre C,Mallet F,Simone RD.Modeling time(s).In:Proc.of the Int’l Conf.on Model Driven Engineering Languages and Systems(Mo DELS).Berlin:Springer-Verlag,2007.559-573.[doi:10.1007/978-3-540-75209-7_38]
[28]Alur R,Dill D.A theory of timed automata.Theoretical Computer Science,1994,126(2):183-235.[doi:10.1016/0304-3975(94)90010-8]
[29]Zhou CC,Hoare CA,Ravn AP.A calculus of duration.Information Processing Letters,1991,40(5):269-276.[doi:10.1016/0020-0190(91)90122-X]
[30]UML Tools.2016.https://www.wikiwand.com/en/List_of_Unified_Modeling_Language_tools
[31]IBM Rational Software.2016.https://www.ibm.com/software/rational
[32]SAP Power Designer.2016.http://go.sap.com/product/data-mgmt/powerdesigner-data-modeling-tools.html
[33]Pragma Dev Studio.2016.http://www.pragmadev.com/
[34]IBM SDL Suite.2016.http://www-01.ibm.com/software/awdtools/sdlsuite/
[35]PAT Model Checker.2016.http://www.patroot.com/
[36]Aceituna D,Do H,Lee SW.SQ2E:An approach to requirements validation with scenario question.In:Proc.of the Int’l Conf.on Asia Pacific Software Engineering.2010.33-42.[doi:10.1109/APSEC.2010.14]
[37]Aceituna D,Do H,Lee SW.Interactive requirements validation for reactive systems through virtual requirements prototype.In:Proc.of the Int’l Conf.on Model-Driven Requirements Engineering Workshop(Mo DRE).2011.1-10.[doi:10.1109/Mo DRE.2011.6045361]
[38]Lee YK,In HP,Kazman R.Customer requirements validation method based on mental models.In:Proc.of the Int’l Conf.on Asia-Pacific Software Engineering Conf.2014.199-206.[doi:10.1109/APSEC.2014.39]
[39]IBM Rational Requisite Pro.http://open-services.net/software/ibm-rational-requisite-pro/
[40]The Pro B Animator and Model Checker.https://www3.hhu.de/stups/prob/
[41]UPPAAL.http://www.uppaal.org/
[42]Maio WK,Pu GG,Yao YB,Su T,Bao DZ,Liu Y.Automated requirements validation for ATP software via specification review and testing.In:Proc.of the Int’l Conf.on Formal Engineering Methods(ICFEM).Springer Int’l Publishing,2016.26-40.[doi:10.1007/978-3-319-47846-3_3]
[43]Frehse G.PHAVer:Algorithmic verification of hybrid systems past Hy Tech.Int’l Journal on Software Tools for Technology Transfer(STTT),2008,10(3):263-279.[doi:10.1007/s10009-007-0062-x]
[44]Podelski A,Rybalchenko A.Transition predicate abstraction and fair termination.ACM SIGPLAN Notices,2005,40(1):132-144.[doi:10.1145/1047659.1040317]
[45]Podelski A,Rybalchenko A.ARMC:The logical choice for software model checking with abstraction refinement.In:Practical Aspects of Declarative Languages.Berlin:Springer-Verlag,2007.245-259.[doi:10.1007/978-3-540-69611-7_16]
[46]Olderog ER.Automatic verification of combined specifications:An overview.Electronic Notes in Theoretical Computer Science,2008,207:3-16.[doi:10.1016/j.entcs.2008.03.082]
[47]Cho C,Choi D,Quan Z,Choi S,Park G,Ryou M.Modeling of CBTC carborne ATO functions using SCADE.In:Proc.of the Int’l Conf.on Control,Automation and Systems.2011.1089-1093.
[48]Simulink.2016.https://www.mathworks.com/products/simulink
[49]Feiler PH,Gluch DP,Hudak JJ.The architecture analysis&design language(AADL):An introduction.Technical Report,CMU/SEI-2006-TN-011,Carnegie Mellon University,2006.
[50]OSATE2.2016.http://osate.github.io/
[51]Li C,Zhang L.Train control system modeling and design based on AADL.In:Proc.of the Int’l Conf.on Software Engineering and Service Science.2015.474-477.[doi:10.1109/ICSESS.2015.7339100]
[52]Ahmad E,Dong YW,Larson B,LüJ,Tang T,Zhan NJ.Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL.Science China Information Sciences,2015,58(11):1-20.[doi:10.1007/s11432-015-5346-2]
[53]Yang CS,Lim JL,Um JK,Han JM,Bang Y,Kim HH,Yun YH,Kim CJ,Cho YJ.Developing CBTC software using model-driven development approach.In:Proc.of the WCRR.2008.
[54]Yang SW.Modeling and safety verification of zone controller in CBTC with UML[MS.Thesis].Beijing:Beijing Jiaotong University,2008(in Chinese with English abstract).
[55]Henzinger TA.The theory of hybrid automata.In:Proc.of the IEEE Symp.on Logic in Computer Science.Berlin:Springer-Verlag,1996.278-292.[doi:10.1007/978-3-642-59615-5_13]
[56]Bu L,Wang Q,Chen X,Wang L,Zhang T,Zhao J,Li X.Toward online hybrid systems model checking of cyber-physical systems’time-bounded short-run behavior.ACM SIGBED Review,2011,8(2):7-10.[doi:10.1145/2000367.2000368]
[57]LüJD,Tang T,Yan F,Xu TH.UPPAAL-Based simulation and verification of CBTC zone control subsystem in rail transportation.Journal of the China Railway Society,2009,31(3):59-64(in Chinese with English abstract).
[58]SCADE Suite.2016.http://www.esterel-technologies.com/products/scade-suite/
[59]Ren X,Zhou MC.Tactical scheduling of rail operations:A Petri net approach.In:Proc.of the Int’l Conf.on Intelligent Systems for the 21st Century.1995.3087-3092.[doi:10.1109/ICSMC.1995.538256]
[60]Hei X,Takahashi S,Nakamura H.Distributed interlocking system and its safety verification.In:Proc.of the Int’l Conf.on Intelligent Control and Automation.2006.8612-8615.[doi:10.1109/WCICA.2006.1713661]
[61]H?rste MM,Schnieder E.Modelling and simulation of train control systems using Petri nets.In:Proc.of the World Congress on Formal Methods.Berlin:Springer-Verlag,1999.1867-1867.[doi:10.1007/3-540-48118-4_58]
[62]Ren GB.Modelling and analysis of high-speed train tracking process based on high-level Petri net.[Ph.D.Thesis].Lanzhou:Lanzhou Jiaotong University,2015(in Chinese with English abstract).
[63]Boudi Z,Collart-Dutilleul S,Khaddour M.High level Petri net modeling for railway safety critical scenarios.In:Proc.of the Int’l Conf.on Formal Methods for Automation and Safety in Railway and Automotive Systems.2014.65-75.
[64]CPN Tool.2016.http://cpntools.org/
[65]Wu DY,Zhang Y.Researching colored Petri nets model of communication based train control system.Journal of System Simulation,2005,17(10):2388-2391(in Chinese with English abstract).
[66]Zhao SX,Wang XL.Movement authority process formal modeling for China train control system-3.Computer Engineering and Design,2013,34(6):2119-2124.
[67]Ahmad E,Dong YW,Larson B,LüJ,Tang T,Zhan NJ.Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL.Science China Information Sciences,2015,58(11):1-20.[doi:10.1007/s11432-015-5346-2]
[68]Sun P,Collart-Dutilleul S,Bon P.A formal modeling methodology of french railway interlocking system via HCPN.WIT Trans.on the Built Environment.2014,135:1-10.[doi:10.2495/CR140711]
[69]Zimmermann A,Hommel G.Towards modeling and evaluation of ETCS real-time communication and operation.Journal of Systems and Software,2005,77(1):47-54.[doi:10.1016/j.jss.2003.12.039]
[70]Zhou G,Zhao HB.Modeling and safety analysis of track occupancy checking logic in section signaling.Journal of the China Railway Society,2016,38(4):66-73(in Chinese with English abstract).
[71]Zhou G,Zhao H.Modeling and quantitative safety analysis of Chinese train control system of systems.In:Proc.of the Int’l Conf.on Intelligent Transportation Systems(ITSC).2015.381-386.[doi:10.1109/ITSC.2015.71]
[72]Rigorous Approach to Industrial Software Engineering.2016.http://spd-web.terma.com/Projects/RAISE/
[73]Haxthausen AE,Peleska J.Formal development and verification of a distributed railway control system.IEEE Trans.on Software Engineering,2000,26(8):687-701.[doi:10.1109/32.879808]
[74]Xu SZ.Modeling and analysis of RBC handover based on timed RAISE[Ph.D.Thesis].Lanzhou:Lanzhou Jiaotong University,2015(in Chinese with English abstract).
[75]PLASMA Lab.2016.https://project.inria.fr/plasma-lab/
[76]Modelica.2016.https://www.modelica.org/
[77]CHARON.2016.https://rtg.cis.upenn.edu/mobies/charon/
[78]Nu SMV.2016.http://nusmv.fbk.eu/
[79]The Coq Proof Assistant.2016.https://coq.inria.fr/
[80]Rodin.2016.http://www.event-b.org/
[81]Probabilistic Symbolic Model Checker.2016.http://www.prismmodelchecker.org
[82]Goodman CJ,Siu LK,Ho TK.A review of simulation models for railway systems.In:Proc.of the Int’l Conf.on Developments in Mass Transit Systems.1998.80-85.[doi:10.1049/cp:19980101]
[83]Cimatti A,Corvino R,Lazzaro A,Narasamdya I,Rizzo T,Roveri M,Tchaltsev A.Formal verification and validation of ERTMS industrial railway train spacing system.In:Proc.of the Int’l Conf.on Computer Aided Verification.Berlin:Springer-Verlag,2012.378-393.[doi:10.1007/978-3-642-31424-7_29]
[84]Hemmat MHA,Mohamed OA,Boukadoum M.Formal modeling,verification and implementation of a train control system.In:Proc.of the Int’l Conf.on Microelectronics(ICM).2015.134-137.[doi:10.1109/ICM.2015.7438006]
[85]Qian J,Liu J,Chen XH,Sun JF.Modeling and verification of zone controller:The SCADE experience in china's railway systems.In:Proc.of the Int’l Workshop on Complex Faults and Failures in Large Software Systems.2015.48-54.[doi:10.1109/COUFLE SS.2015.15]
[86]Platzer A.Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics.Berlin:Springer-Verlag,2010.[doi:10.1007/978-3-642-14509-4]
[87]Zou L,Zhan NJ,Wang SL,Fr?nzle M,Qin SC.Verifying simulink diagrams via a hybrid Hoare logic prover.In:Proc.of the Int’l Conf.on Embedded Software,Vol.9.2013.1-10.[doi:10.1109/EMSOFT.2013.6658587]
[88]Zhou X,Zhang Y.Security analysis about a train control center based on a Bayesian network.In:Proc.of the Int’l Conf.on Transportation Engineering.Reston:American Society of Civil Engineers.2015.
[89]Xu TH,Tang T,Gao CH,Cai BG.Dependability analysis of the data communication system in train control system.Science in China Series E:Technological Sciences,2009,52(9):2605-2618.[doi:10.1007/s11431-009-0183-4]
[90]Zhao HL,Xu TH,Tang T.Towards modeling and evaluation of availability of communication based train control(CBTC)system.In:Proc.of the Int’l Conf.on Communication Technology and Applications.2009.860-863.[doi:10.1109/ICCOMTA.2009.5349076]
[91]Bu L,Wang Q,Chen X,Wang L,Zhang T,Zhao J,Li X.Toward online hybrid systems model checking of cyber-physical systems’time-bounded short-run behavior.ACM SIGBED Review,2011,8(2):7-10.[doi:10.1145/2000367.2000368]
[92]LüJD,Tang T,Yan F,Xu TH.UPPAAL-Based simulation and verification of CBTC zone control subsystem in rail transportation.Journal of the China Railway Society,2009,31(3):59-64(in Chinese with English abstract).
[93]David A,Du D,Larsen KG,Legay A,Miku?ionis M.Optimizing control strategy using statistical model checking.In:Proc.of the NASA Formal Methods Symp.Berlin:Springer-Verlag,2013.352-367.[doi:10.1007/978-3-642-38088-4_24]
[94]Gu F,Zhang XQ,Chen MS,Grosse D,Drechsler R.Quantitative timing analysis of UML activity diagrams using statistical model checking.In:Proc.of the Int’l Conf.on Design,Automation&Test in Europe Conf.&Exhibition(DATE).2016.780-785.[doi:10.3850/9783981537079_0339]
[95]Mc Dermid J,Kelly T.Software in safety critical systems-achievement and prediction.Nuclear Future,2006,(2):140-146.[doi:10.1680/nuen.2006.2.3.140]
[96]Ellims M.On wheels,nuts and software.In:Proc.of the Australian Workshop on Safety Critical Systemsand Software.Parlinghurst:Austranlian Computer Society,2004.67-76.
[97]Heimdahl MPE.Safety and software intensive systems:Challenges old and new.In:Proc.of the Future of Software Engineering.2007.137-152.[doi:10.1109/FOSE.2007.18]
[98]Lutz RR.Software engineering for safety:A roadmap.In:Proc.of the Future of Software Engineering.New York:ACM,2000.213-226.[doi:10.1145/336512.336556]
[99]Leea JH,Hwanga JG,Shina D,Leea KM,Kimb SU.Development of verification and conformance testing tools for a railway signaling communication protocol.Computer Standards and Interfaces,2009,31(2):362-371.[doi:10.1016/j.csi.2008.05.011]
[100]Didrich K,Herbs S,Vieria M.Applying model-based testing to a train control system.In:Proc.of the INFORMATIK.2006.249-256.
[101]Zhang Y.Fault related formal test method of the software in train control system[Ph.D Thesis].Beijing:Beijing Jiaotong University,2012(in Chinese with English abstract).
[102]UPPAAL-TRON.2016.http://people.cs.aau.dk/~marius/tron/
[103]UPPAAL Cover.http://www.hessel.nu/Co Ver/
[104]Hessel A,Larsen KG,Mikucionis M,Nielsen B,Pettersson P,Skou A.Testing real-time systems using UPPAAL.In:Proc.of the Formal Methods and Testing.2008.77-117.[doi:10.1007/978-3-540-78917-8_3]
[105]LüJD,Zhu XL,Wang HF,Li KC,TANG T.Research on conformance testing for nondeterministic delay in high speed train control system based on UPPAAL-TRON.Journal of the China Railway Society,2016,38(1):54-64(in Chinese with English abstract).
[106]LüJD,Ren PC,Lei C,Li KC,Tang T.Model-Based test case generation for function testing of CTCS-3 onboard subsystem.Journal of Control and Automation,2015,8(1):171-178.[doi:10.14257/ijca.2015.8.10.17]
[107]Yang L,LüJD,L Y,Li CL,Zhao WH.Research on model-based test case generation method of onboard subsystem in CTCS-3.Journal of the China Railway Society,2014,36(8):55-62(in Chinese with English abstract).
[108]Chen X,Jang P,Zhang YF,Huang C,Zhou Y.Method of automatic test case generation for safety-critical scenarios in train control systems.Ruan Jian Xue Bao/Journal of Software,2015,26(2):269-278(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/4780.htm[doi:10.13328/j.cnki.jos.004780]
[109]Yin YF,Liu B,Ni HY.Real-Time embedded software testing method based on extended finite state machine.Journal of Systems Engineering and Electronics,2012,23(2):276-285.[doi:10.1109/JSEE.2012.00035]
[110]Hilken C,Hübner F,Peleska J.Combination of behavioral and parametric diagrams for model-based testing.Technical Report,open ECTS Report 2014-11-25,University of Bremen,2015.
[111]Ministry of Railway of the People’s Republic of China.TB/T 2615-1994 Railway Signal Failure—Safety Principles.Beijing:China Railway Publishing House,1995(in Chinese).
[112]Morell LJ.A theory of fault-based testing.IEEE Trans.on Software Engineering,1990,16(8):844-857.[doi:10.1109/32.57623]
[113]Tu HY,Wu FM.Embedding fault in simulation environment for software black-box testing.Ruan Jian Xue Bao/Journal of Software,1998,10(5):516-520(in Chinese with English abstract).
[114]Gay G,Staats M,Whalen M,Heimdahl M.The risks of coverage-directed test case generation.IEEE Trans.on Software Engineering,2015,41(8):803-819.[doi:10.1109/TSE.2015.2421011]
[115]Baker R,Habli I.An empirical evaluation of mutation testing for improving the test quality of safety-critical software.IEEE Trans.on Software Engineering,2013,39(6):787-805.[doi:10.1109/TSE.2012.56]
[116]Sun HY,Chen MS,Zhang M,Liu J,Zhang Y.Improving defect detection ability of derived test cases based on mutated UML activity diagrams.In:Proc.of the Annual Computer Software and Applications Conf.2016.275-280.[doi:10.1109/COMPSAC.2016.136]
[117]Li T,Li KC,Lv JD,Yuan L,Fu Q,Wen T.Mutation testing for evaluating the completeness of test cases in high-speed train control system.In:Proc.of the Int’l Conf.on Intelligent Transportation Systems.2015.777-782.[doi:10.1109/ITSC.2015.131]
[118]Wang X,Ma LC,Tang T.Study on formal modeling andverification of safety computer platform.Advances in Mechanical Engineering,2016,8(5):1-13.[doi:10.1177/1687814016649115]
[119]Lu QJ.Modeling and analysis of CBTC onboard equipment based on colored Petri net[MS.Thesis].Beijing:Beijing Jiaotong University,2008(in Chinese with English abstract).
[120]Zhu L,Ning B.The design of the CBTC train-ground communication system based on IEEE 802.11g standard.China Railway Science,2010,31(5):119-124(in Chinese with English abstract).
[1]郜春海.自主创新CBTC系统的核心技术研究.都市快轨交通,2011,24(4):1-4.
[3]曹源,唐涛,徐田华,穆建成.形式化方法在列车运行控制系统中的应用.交通运输工程学报,2010,10(1):112-126.
[4]唐涛,赵林编.基于模型的列车运行控制系统设计与验证方法.北京:中国铁道出版社,2014.
[7]胡雪莲.基于UML和UPPAAL的CTCS-3级列控系统等级转换场景建模与验证[硕士学位论文].兰州:兰州交通大学,2015.
[8]刘金涛,唐涛,徐田华,赵林.基于UML的CTCS-3级列控系统需求规范形式化验证方法.中国铁道科学,2011,32(3):93-99.
[10]张庆新.基于x UML的列控系统需求规范验证方法研究[硕士学位论文].北京:北京交通大学,2011.
[12]何丽芸,赵林,程瑞军.属性驱动的列车控制系统需求建模与验证.铁路计算机应用,2014,(2):1-6.
[13]程瑞军,赵林,何丽芸.基于UML及属性的需求分析方法在列控系统需求规范中的应用.铁道通信信号,2013,(2):80-84.
[25]刘金涛.基于STPA的需求阶段的高速列车运行控制系统安全分析方法研究[博士学位论文].北京:北京交通大学,2015.
[54]杨旭文.基于UML的CBTC系统区域控制器的建模与安全性验证[硕士学位论文].北京:北京交通大学,2008.
[57]吕继东,唐涛,燕飞,徐天华.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证.铁道学报,2009,31(3):59-64.
[62]任国彬.基于高级Petri网的高速列车追踪运行过程建模与分析[硕士学位论文].兰州:兰州交通大学,2015.
[65]吴东勇,张勇.基于通信的列车控制系统的有色Petri网模型的研究.系统仿真学报,2005,17(10):2388-2391.
[70]周果,赵会兵.区间占用检查逻辑的建模与安全分析.铁道学报,2016,38(4):66-73.
[74]徐世泽.基于Timed RAISE的RBC切换建模与分析[硕士学位论文].兰州:兰州交通大学,2015.
[101]张岩.列车运行控制系统软件故障相关形式化测试方法[博士学位论文].北京:北京交通大学,2012.
[105]吕继东,朱晓琳,王海峰,李开成,唐涛.基于UPPAAL-TRON的高速铁路列控系统非确定性时延一致性测试研究.铁道学报,2016,38(1):54-64.
[107]袁磊,吕继东,刘雨,李辰岭,赵伟慧.一种全覆盖的列控车载系统测试用例自动生成算法研究.铁道学报,2014,36(8):55-62.
[108]陈鑫,姜鹏,张一帆,黄超,周岩.一种面向列车控制系统中安全攸关场景的测试用例自动生成方法.软件学报,2015,26(2):269-278.http://www.jos.org.cn/1000-9825/4780.htm[doi:10.13328/j.cnki.jos.004780]
[111]中华人民共和国铁道部.TB/T 2615-1994铁道信号故障——安全原则.北京:中国铁道出版社,1995.
[119]陆启进.基于有色Petri网的CBTC车载设备应用软件的建模与分析[硕士学位论文].北京:北京交通大学,2008.
[120]朱力,宁滨.基于IEEE 802.11g标准的CBTC车地通信系统设计.中国铁道科学,2010,31(5):119-124.