列车运行控制系统分层形式化建模与验证分析
|
摘要
列车运行控制系统(简称“列控系统”)是将先进的控制技术、通信技术、计算机技术与铁路信号技术融为一体,保证轨道交通安全、正点、高密度运行的自动化系统。随着计算机在列控系统中的广泛应用,硬件和软件规模不断扩大,系统的复杂性有了很大的提高,呈现出复杂的系统特性(并发性、实时性和混合属性等等)。作为一个复杂安全苛求系统,列控系统中任何故障都有可能造成重大的人身伤亡和财产损失,如何保证系统的正确性,寻找一套全面的、有效的建模与验证方法是非常必要的。相比仿真和测试技术,基于严格数学定义的形式化方法不仅能精确、清晰地描述系统结构和相关特性,而且能对特性进行验证,近年来已经成为列控系统建模和验证的一种重要理论方法。
论文引入系统层次化建模概念,利用面向对象的建模思想和基于场景的系统设计理念,提出了一套包含系统层、场景层、组件层和功能层的列控系统层次化模型。在此基础上,提出了一个集成HCSP(Hybrid Communication Sequential Process)、CHARON和TL (Temporal Logic)的列控系统分层形式化建模与验证框架。该框架不仅适合列控系统各种特性的验证分析,而且建立的模型具有可继承性、重用性,在保证系统模型一致性的基础上,提高了建模的效率。
论文深入分析了列控系统运营场景实时性的验证问题,提出了六种适合于列控系统运营场景描述的时间约束类型：周期性、延迟、时间等待、超时、截止期限和时间中断；提出了HCSP的子集模型到时间自动机网络模型的转换规则；给出了运营场景实时性约束的TCTL (Timed Computation Tree Logic)描述；实现了运营场景中相关实时属性的验证流程。
论文深入研究了列控系统运营场景的混合属性验证问题,指出了传统的混杂系统建模与验证方法在刻画列控系统场景中通信行为上存在的不足。并根据现有HCSP方法的不足,提出了HCSP的假设条件；结合混合自动机的语义,提出了HCSP模型到混合自动机模型的转换规则；给出了运营场景中混合属性的ACTL (Action Computation Tree Logic)表达；实现了运营场景中相关混合属性的验证流程。
论文最后选取了CTCS-3级列控系统总体技术方案中两个典型的运营场景(RBC (Radio Block Center)切换场景和行车许可场景)作为案例来分析。通过对RBC切换场景和行车许可场景的分层形式化建模与验证分析,验证了列控系统的实时性和混合属性,最大限度的避免了系统设计上的缺陷和错误,为进一步解决列控系统建模与验证的关键理论问题,保障列控系统安全可靠的应用和运营提供重要的理论基础。
The Train Control System is an automatic system which is integrated of advanced control technology, advanced communication technology, advanced computer technology and railway signal technology. It plays an important role in assuring safety and improving efficiency in railway. The increasing usage of computer technology has led to the increasing complexity in the train control system with large scale of software and hardware, which has exhibited highly distributed, real-time, safety and hybrid properties. As a complex safety-critical system, any fault in train control system can lead to huge human injury or wealth losing. It is necessary to find a more effective and across-the-aboard modeling and verification methodology to guarantee the correctness of train control system. As is compared to simulation technology and testing technology, formal methods based on rigorous mathematics definition have become an important modeling and verification theory in the field of train control systems due to its accurate and clear description of system architecture and related characteristics.
A hierarchical model of train control system including system layer, scenario layer, component layer and function layer is proposed firstly by introducing hierarchical modeling conception, using object-oriented methodology and scenario-based design methodology. Based on the hierarchical model, a hierarchical formal modeling and verification framework which is integrated of HCSP, CHARON and TL is proposed. It is not only suitable for verifying all the characteristics of train control system, but also improves the modeling efficiency due to its hierarchical and reused characteristics.
The real-time properties of operation scenario in train control system are deeply researched. Six time constraints stated in terms recursion, delay, wait until, time-out, deadline and time interrupt are proposed. Some transition rules are introduced for transiting the HCSP subset models to TA network models. The real-time properties of operation scenario are described using TCTL, and finally a procedure is given for verification based on the simulation.
The hybrid properties of operation scenario in train control system are deeply researched. It is pointed that the traditional formal methods of hybrid system are not well in describing communication behaviors which occur in the interactive process of subsystems. To overcome this problem, we introduce a formal modeling and verification method by extending the HCSP syntax and semantics. We transit the HCSP models to HA models by introducing some transition rules based on some assumptions. The hybrid properties of operation scenarios are described using ACTL, and finally a procedure is given for verification based on the simulation.
Finally, two typical cases of operation scenario which are RBC handover scenario and movement authority scenario are chosen according to the general technical programming of CTCS level 3 train control system in railways for passengers. Based on the two hierarchical formal modeling and verification models, the real-time and hybrid properties of CTCS-3 train control system are separated verified. As a result, it avoids the maximum fault and error in the system design. It is considered that the method is powerful for solving the key problems in modeling and verification train control system. It is of great significance for ensuring the safety and reliability in train control system.
论文引入系统层次化建模概念,利用面向对象的建模思想和基于场景的系统设计理念,提出了一套包含系统层、场景层、组件层和功能层的列控系统层次化模型。在此基础上,提出了一个集成HCSP(Hybrid Communication Sequential Process)、CHARON和TL (Temporal Logic)的列控系统分层形式化建模与验证框架。该框架不仅适合列控系统各种特性的验证分析,而且建立的模型具有可继承性、重用性,在保证系统模型一致性的基础上,提高了建模的效率。
论文深入分析了列控系统运营场景实时性的验证问题,提出了六种适合于列控系统运营场景描述的时间约束类型：周期性、延迟、时间等待、超时、截止期限和时间中断；提出了HCSP的子集模型到时间自动机网络模型的转换规则；给出了运营场景实时性约束的TCTL (Timed Computation Tree Logic)描述；实现了运营场景中相关实时属性的验证流程。
论文深入研究了列控系统运营场景的混合属性验证问题,指出了传统的混杂系统建模与验证方法在刻画列控系统场景中通信行为上存在的不足。并根据现有HCSP方法的不足,提出了HCSP的假设条件；结合混合自动机的语义,提出了HCSP模型到混合自动机模型的转换规则；给出了运营场景中混合属性的ACTL (Action Computation Tree Logic)表达；实现了运营场景中相关混合属性的验证流程。
论文最后选取了CTCS-3级列控系统总体技术方案中两个典型的运营场景(RBC (Radio Block Center)切换场景和行车许可场景)作为案例来分析。通过对RBC切换场景和行车许可场景的分层形式化建模与验证分析,验证了列控系统的实时性和混合属性,最大限度的避免了系统设计上的缺陷和错误,为进一步解决列控系统建模与验证的关键理论问题,保障列控系统安全可靠的应用和运营提供重要的理论基础。
The Train Control System is an automatic system which is integrated of advanced control technology, advanced communication technology, advanced computer technology and railway signal technology. It plays an important role in assuring safety and improving efficiency in railway. The increasing usage of computer technology has led to the increasing complexity in the train control system with large scale of software and hardware, which has exhibited highly distributed, real-time, safety and hybrid properties. As a complex safety-critical system, any fault in train control system can lead to huge human injury or wealth losing. It is necessary to find a more effective and across-the-aboard modeling and verification methodology to guarantee the correctness of train control system. As is compared to simulation technology and testing technology, formal methods based on rigorous mathematics definition have become an important modeling and verification theory in the field of train control systems due to its accurate and clear description of system architecture and related characteristics.
A hierarchical model of train control system including system layer, scenario layer, component layer and function layer is proposed firstly by introducing hierarchical modeling conception, using object-oriented methodology and scenario-based design methodology. Based on the hierarchical model, a hierarchical formal modeling and verification framework which is integrated of HCSP, CHARON and TL is proposed. It is not only suitable for verifying all the characteristics of train control system, but also improves the modeling efficiency due to its hierarchical and reused characteristics.
The real-time properties of operation scenario in train control system are deeply researched. Six time constraints stated in terms recursion, delay, wait until, time-out, deadline and time interrupt are proposed. Some transition rules are introduced for transiting the HCSP subset models to TA network models. The real-time properties of operation scenario are described using TCTL, and finally a procedure is given for verification based on the simulation.
The hybrid properties of operation scenario in train control system are deeply researched. It is pointed that the traditional formal methods of hybrid system are not well in describing communication behaviors which occur in the interactive process of subsystems. To overcome this problem, we introduce a formal modeling and verification method by extending the HCSP syntax and semantics. We transit the HCSP models to HA models by introducing some transition rules based on some assumptions. The hybrid properties of operation scenarios are described using ACTL, and finally a procedure is given for verification based on the simulation.
Finally, two typical cases of operation scenario which are RBC handover scenario and movement authority scenario are chosen according to the general technical programming of CTCS level 3 train control system in railways for passengers. Based on the two hierarchical formal modeling and verification models, the real-time and hybrid properties of CTCS-3 train control system are separated verified. As a result, it avoids the maximum fault and error in the system design. It is considered that the method is powerful for solving the key problems in modeling and verification train control system. It is of great significance for ensuring the safety and reliability in train control system.
引文
[1]唐涛,徐田华,赵林.列车运行控制系统规范建模与验证[M].北京：中国铁道出版社,2010.
[2]徐田华.概率模型检验及其在列车运行控制系统中的应用[D].北京：北京交通大学博士后出站报告.2007.
[3]燕飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究.北京：北京交通大学博士论文,2006.
[4]员春欣.铁路信号容错技术[M].北京：中国铁道出版社,1997.
[5]王海峰.安全关键系统的形式化开发方法研究.北京：北京交通大学博士论文,2002.
[6]古天龙.软件开发的形式化方法[M].北京：高等教育出版社,2005.
[7]张曙光.京沪高速铁路系统优化研究[M].北京：中国铁道出版社,2009.
[8]丁建文,蒋文怡,钟章队GSMR移动通信网络与列车控制系统的发展[J].中国铁路,2007,(2)：46-47.
[9]J. Hoenicke, P. Maier. Model-Checking of Specification Integrating Processes, Data and Time. http://www.springerlink.com/index/98X8PV7APVDTKAGM.pdf.
[10]J.Hoenicke and E.-R.Olderog. CSP-OZ-DC:A combination of specification techniques for processed, data and time. Nordic Journal of Computing,9(4):301-334,2002. Appear March 2003.
[11]D.Craigen. Formal Methods, EVES, and Safety Critical Systems. Technical Report FR-94-5479-04[R].Minister of National Defence, Ontario, Canada,1994.
[12]Y. Papadopoulos, J.A.McDermid. The Potential for a Generic Approach to Certification of Safety Critical Systems in the Transportation Sector[J]. Reliability Engineering and Systems Safety, 1999,63(1):47-66.
[13]Neil Storey. Safety-Critical Computer Systems[M]. Addison-Wesley,1996.
[14]曹源,唐涛,徐田华,穆建成.形式化方法在列车运行控制系统中的应用[J].交通运输工程学报,2010,10(1)：114-115.
[15]CENELEC EN50129-2003. Railway applications-Communication. signalling and processing systems-Safety related electronic systems for signalling[S]. BSI.2003.
[16]IEC. IEC61508:2005. Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems[S]. IEC.2005.
[17]ERTMS Users Group. ERTMS/ETCS System Requirement Specification class1; subset-026.
[18]ERTMS Users Group. ERTMS/ETCS Function Requirement Specification FRS.
[19]李晓山,周巢尘.时段演算综述[J].计算机学报,1994,11,842-851.
[20]Chaochen Z, Hansen M. Duration Calculus-A Formal Approach to Real-Time Systems[M]. Springer-Verlag,2003.
[21]Roland Meyer. Model-Checking von Phasen-Event-Automaten bezuglich, Duration Calculus Formeln mittels Testautomaten[D]. Ph.D Thesis of UniversitAat Oldenburg, Aug 2005.
[22]A. Schafer. Combining Real-Time Model-Checking and Fault Tree Analysis. In Proc. Formal Methods Europe (FM 2003), vol.2805 of LNCS, pp.522-541. Springer,2003.
[23]R. Meyer, J. Faber, and A. Rybalchenko. Model checking duration Calculus:a practical approach. In:K. Barkaoui,A. Cavalcanti, and A. Cerone (Eds.),Proc. Int'l Coll. on Theoret.Aspects of Computing (ICTAC),vol.4281 of Lecture Notes in Computer Science, pp.332-346.Springer, 2006.
[24]S.Veloudis,N.Nissanke. Duration Calculus in the specification of safety requirement.Proceedings of the 5th International Symposim on Formal Techniques in Real-Time and Fault-Tolerant System, LCNS, vol.1486, pp.13-112,1998.
[25]Kirsten Berkenkotter Stefan Bisanz Ulrich Hannemann Jan Peleska. The HybridUML profile for UML 2.0[J]. International Journal on Software Tools for Technology (2006) 8(2):167-176
[26]Kirsten Berkenkotter Stefan Bisanz Ulrich Hannemann Jan Peleska. HybridUML profile for UML2.0. SVERTS Workshop at the UML 2003 Conference, October 2003. http://www.verimag. imag.fr/EVENTS/2003/SVERTS/.
[27]Paul Ziemann and Martin Gogolla. Validating OCL specifications with the USE tool-an example based on the BART case study. In Thomas Arts and Wan Fokkink, editors, Proc.8th Int. Workshop Formal Methods for Industrial Critical Systems (FMICS'2003), volume 80 of ENTCS. Elsevier,2003.
[28]Andr'e Platzer. Differential Dynamic Logic for Verifying Parametric Hybrid Systems[J]. Automated Reasoning with Analytic Tableaux and Related Methods, Springer Berlin/Heidelberg 2007, pp.216-232.
[29]Andr'e Platzer. A Temporal Dynamic Logic for Verifying Hybrid System Invariants[J]. Logical Foundations of Computer Science, Springer Berlin/Heidelberg 2007, pp.457-471.
[30]Andr'e Platzer, Jan-David Quesel. Logical Verification and Systematic Parametric Analysis in Train Control[J]. Lecture Notes in Computer Science[J], Springer Berlin 2008, pp.646-649.
[31]Andr'e Platzer, Jan-David Quesel. European Train Control System:A Case Study in Formal Verification [J]. Lecture Notes in Computer Science[J], Springer Berlin 2009, pp.246-265.
[32]Damm, W., Hungar, H., Olderog, E.-R.:Verification of cooperating traffic agents. International Journal of Control 79(5),395-421 (2006).
[33]Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rudiger Olderog, Jun Pang, Andre Platzer, Marc Segelken, and BorisWirtz. Automating Verification of Cooperation, Control, and Design in Traffic Applications [J]. Springer Berlin 2007, pp.115-169.
[34]Kapur D, Winter V L. On the construction of a domain language for a class of reactive systems [C]//Winter Victor L, Bhattacharya Sourav. The Kluwer International Series In Engineering And Computer Science. Massachusetts. Kluwer Academic Publishing.2001:169-196.
[35]Winter V L, Kapur D, R.S.Berg. A refinement-based approach for developing software controllers for train systems [C]//Winter Victor L, Bhattacharya Sourav. The Kluwer International Series In Engineering And Computer Science. Massachusetts. Kluwer Academic Publishing.2001:197-240.
[36]Winter V L, Kapur D,Fuehrer G. Formal specification and refinement of a safe train control function. [C]//Fsbrice Kordon Formal,Michel Lemoine.Methods for Embedded Distributed Systems:How to Master the Complexity. Massachusetts. Kluwer Academic Publishing.2004:25-64.
[37]Morten P. Lindegaard. Proof Support for RAISE[D].Kongens Lyngby. PH.D Thesis of Technical University of Denmark.2004.
[38]Meyer H M,Schnieder E. Modelling and Simulation of Train Control Systems using Petri Nets [C]//Trier University. Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Toulouse. Springer.1999:1867-1883.
[39]Jansen L,Meyer H M,Schnieder E. Technical Issues in Modelling the European Train Control Systems (ETCS) Using Coloured Petri Nets and Design/CPN Tools [R]//Aarhus Universitet. Workshop on Practical Use of Coloured Petri Nets and Design. Aarhus.1998:103-115.
[40]Michael Meyer zu Horste and Eckehard Schnieder. Modeling train control systems with Petri nets-A functional reference-architecture[C].2000 IEEE International Conference on System,man and Cybernetics. Nashville, TN, USA,2000:3081-3086.
[41]Kirsten Berkenkotter Stefan Bisanz Ulrich Hannemann Jan Peleska. Executable HybridUML and its Application to Train Control Systems.2004, LNCS 3147, pp.145-173.
[42]Paul Ziemann and Martin Gogolla. Validating OCL specifications with the USE tool-an example based on the BART case study[C]. In Thomas Arts and Wan Fokkink, editors, Proc.8th Int. Workshop Formal Methods for Industrial Critical Systems (FMICS'2003), volume 80 of ENTCS. Elsevier,2003.
[43]CONTRACT ERA/2007/ERTMS/02. ETCS tool architecture description. http://www.era.europa.eu/core/ertms/.../ETCS_architecture_v_1_0.pdf.
[44]Eckehard Schnieder, Mourad Chouikha, Stefan Einer and Michael Meyer zu Horste BASYSNET-An Integrated Approach for Automated Control System Development[C]. Petri Net Technology for Communication-Based Systems. Lecture Notes in Computer Science,2003, Volume 2472/2003,352-362.
[45]Michael Meyer zu Horste, Srinivasan Parthasarathy, Eckehard Schnieder. NOTATION,METHOD,TOOL:A CONCEPTUAL FRAMEWORK FOR THE APPLICATION OF FORMAL METHODS[C].2000 IFAC Control in Transportations Systems, braunschhweig,Germany, 2000,pp:113-118.
[46]Haxthausen A.E, Peleska J. Formal Development and Verification of a Distributed Railway Control System[J]. IEEE Transactions On Software Engineering.2000.26 (8):687-701.
[47]吕继东,唐涛,燕飞,徐田华.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证[J].铁道学报,2009,31(3)：59-64.
[48]吕继东,唐涛,贾吴.客运专线CTCS-3级列控系统无线闭塞中心的建模与验证[J].铁道学报,2010,32(6)：34-42.
[49]牛儒,曹源,唐涛ETCS-2级列控系统RBC交接协议的形式化分析[J].铁道学报,2009,31(4)：52-58.
[50]Jones CB. Systematic Software Development Using VDM.PHI Ltd1990.
[51]Splvey JM. The Z notation:A Reference Manual. Englewood Cliffs. NJ:Prentice Hall 1993.
[52]Chris George.Tutorial on the RAISE Language[C]//Method and Tools Formal Methods and Software Engineering.Berlin.Springer/Heidelberg.2004:3-4
[53]E.H. Dtlrr and J. van Katwijk. VDM++:A Formal Specification Language for Object-Oriented Designs. Computer Systems and Software Engineering, pages 214-219 IEEE Computer Society Press,1992. Proceedings of CompEuro'92.
[54]P.A. Swatman, P.M.C. Swatman, and R. Duke Electronic Data Interchange:A High-level Formal Specification in Object-Z Proceedings of 6th Australian Software Engineering Conference, pages 341-354, Sydney, Australia, Springer-Verlag,1991.
[55]K.Lano. Z++:An Object-Oriented Extension to Z. Proceedings of the 4th Annual Z user Meeting, Oxford, J.E.Nicholls(Ed.), Springer-Verlag,1001, pages 151-172.
[56]HOARE C.A.R. Communicating sequential processes [J]. Communications of the ACM.
[57]R. Gerber and I. Lee. CCSR:A Calculus for Communicating Shared Resources. In Proceedings of CONCUR'90, Lecture Notes in Computer Science, Vol.458, Springer-Verlag,1990, pages 263-277.
[58]Zhou Chaochen,WangJi and Anders P.Ravn A Formal Description of Hybrid Systems[C]. in the Proc of the DIMACS/SYCON workshop on Hybrid systems III:verification and control:verification and control Springer-Verlag New York, Inc. Secaucus, NJ, USA,1996.
[59]Claude Girault, Rudiger Valk.Petri.Nets for System Engineering-A guide to Modeling, Verification, and Applications. Springer 2003.
[60]Jensen,K. Coloured Petri Nets-Basic Concepts, Analysis Methods and Pratical Use. Volume 1 of EATCS Monographs of Theoretical Computer Science, Springer, New York.
[61]肖兵,瞿坦,王明哲.着色Petri网及其在系统建模与仿真中的应用[J].计算机工程,2001,27(1)：30-33.
[62]林闯.随机Petri网和系统性能评价[M].北京：清华大学出版社,2005.
[63]Rajeev Alur, Thao Dang, Joel M. Esposito, Rafael B. Fierro, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George J. Pappas, Oleg Sokolsky. Hierarchical Hybrid Modeling of Embedded Systems. In Proceedings of EMSOFT'2001. pp.14-31.
[64]Rajeev Alur, Radu Grosu, Yerang Hur, Vijay Kumar, Insup Lee. Modular Specification of Hybrid Systems in CHARON. In Proceedings of HSCC'2000. pp.6-19.
[65]Yerang Hur, Rafael B. Fierro, Insup Lee. Modeling Distributed Autonomous Robots Using CHARON:Formation Control Case Study. In Proceedings of ISORC'2003. pp.93-98.
[66]E. Clarke and E. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Proceedings of the Workshop on Logic of Programs. LNCS, vol. 131, pp.52-71.Springer-Verlag,1981.
[67]P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming. LNCS, vol.137,pp.337-351, Springer-Verlag, April 1982.
[68]R.Alur, C. Courcoubetis, and D.L. Dill. Model-checking in dense real-time. In formation and Computation,104:2-34,1993.
[69]G. J. Holzmann and D. Peled. The State of SPIN. In Proceedings of the 8th International Conference on Computer-Aided Verification. R. Alur and T. A.Henzinger, Eds. LNCS, vol.1102, pp. 385-389, Springer-Verlag, August 1996.
[70]Behrmann. G, Larsen. K.G, Moller. O, Divid..A, Pettersson.P and Wang Yi, UPPAAL-present and future[C]//In the Proc of the 40th IEEE Conference on Decision and Control Orlando, Florida USA, December 2001, pp.2881-2886.
[71]Goran Frehse. PHAVer:Algorithmic verification of hybrid systems past HyTech. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems:Computation and Control (HSCC'05), Mar.9-11, 2005, Zurich, CH, volume 2289 of LNCS. Springer,2005. PHAVer is available at http://www.cs.ru.nl/-goranf/.
[72]M. J. Gordon. HOL:a proof generating system for higher-order logic. In G.Biriwistle and P.anyam, editors VLSI Specification, Verification and Synthesis, pp.74-128. Kluwer Academic Publishers,1988.
[73]R.S. Boyer and J.S.Moore. A Theorem Prover for a Computational Logic.In Proceedings of the 10th International Conference on Automated Deduction, LNCS Vol.449, pp.1-15,Springer-Verlag, 1990.
[74]S. Owre, J. M. Rushby, N.Shankar and M. K. Srivas. A Tutorial on Using PVS for Hardware Verification. In Proceedings of the 2nd International Conference of Theorem Provers in Circuit Design:Theory, Practice and experience. LNCS, vol 901, pp.258-279, Springer-Verlag,1994.
[75]刘兴堂.复杂系统建模理论、方法和技术[M].北京：科学出版社,2008.
[76]刘晨.基于SEB组合框架的导弹体系对抗仿真方法研究.长沙：国防科技大学博士论文,2005.
[77]铁道部科技司CTCS-3级列控系统标准规范-客运专线CTCS-3级列控系统运营规则[M].北京：中国铁道出版社,2009.
[78]铁道部科技司CTCS-3级列控系统标准规范-CTCS-3级列控系统功能需求规范(FRS)[M].北京：中国铁道出版社,2009.
[79]铁道部科技司CTCS-3级列控系统标准规范-CTCS-3级列控系统系统需求规范(SRS)(第一册)[M].北京：中国铁道出版社,2009.
[80]铁道部科技司CTCS-3级列控系统标准规范-CTCS-3级列控系统系统需求规范(SRS)(第二册)[M].北京：中国铁道出版社,2009.
[81]铁道部科技司CTCS3级列控系统标准规范系列-CTCS-3级列控系统GSM-R网络需求规范(V1.0)[M].北京：中国铁道出版社,2008.
[82]铁道部科技司CTCS-3级列控系统标准规范系列—无线闭塞技术规范[M].北京：中国铁道出版社,2008.
[83]铁道部科技司CTCS-3级列控系统标准规范系列—-CTCS-3级列控系统应答器工程应用原则[M].北京：中国铁道出版社,2008.
[84]张曙光CTCS-3级列控系统总体技术方案[M].北京：中国铁道出版社,2008.
[85]Rumbaugh,J.etal. Object-oriented Modelling and Design. Prentice Hall, New Jersey.
[86]黄永忠等.面向对象技术与方法概论[M].北京：国防工业出版社,2002.
[87]胡军.构件化嵌入式软件设计的分析与验证.南京：南京大学博士论文,2005.
[88]刘志强.普适计算环境下基于场景的可配置服务研究[D].上海：上海交通大学博士论文,2007.
[89]Amir Pnueli. The Temporal Logic of Programs. In Proceedings of FOCS' 1977. pp.46-57.
[90]Edmund M. Clarke, Orna Grumberg, David E. Long. Model checking. In Proceedings of NATO ASI DPD'1996. pp.305-349.
[91]Clarke, E.M., Emerson, E.A., Sistla, A.P.:Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst.(1986) 244-263.
[92]Zhou Chaochen, C. A. R. Hoare, Anders P. Ravn. A Calculus of Durations. Inf. Process. Lett., 1991:269-276.
[93]Chaochen, Z., Hansen, M.R., Ravn, A.P., and Rischel, H. Duration Specifications for Shared Processors. In Proceedings of FTRTFT.1992,21-32.
[94]Chaochen, Z., Ravn, A.P., and Hansen, M.R. An Extended Duration Calculus for Hybrid Real-Time Systems. In Proceedings of Hybrid Systems.1992,36-59.
[95]Rajeev Alur, David L. Dill. A Theory of Timed Automata. Theor. Comput. Sci.,1994:183-235.
[96]Thomas A. Henzinger, The Theory of Hybrid Automata Logic in Computer Science [A]. LICS'96, Proceedings of Eleventh Annual IEEE Symposium on[C].1996.278-292.
[97]李慧芳,范玉顺.工作流系统时间管理[J].软件学报,2002,13(8)：1552-1557.
[98]冯林,姜浩.基于时间约束Petri网的工作流可调度性分析[J].计算机技术与发展,2006,16(11)：33-37.
[99]龙世荣,张广泉,汀宏海.基于时间自动机的实时工作流时序约束一致性验证[J].苏州大学学报.2009,29(6)：12-16.
[100]刘键,朱晓梅.分布式实时处理形式开发技术导论[J].计算机科学,1995,22(6)：62-73.
[101]吴瑞强.控制系统的实时性研究与优化.浙江：浙江大学博士论文,2006.
[102]李广元LTLC面向实时与混成系统的连续时序逻辑[D].北京：中国科学研究院,2001：10-11.
[103]Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, and Wang Yi. Timed Automata Patterns[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING.2008. pp.844-845.
[104]OUAKNINE J, WORRELL J. Timed CSP=Closed Timed Automata [C]. Brno:Proc of EXPRESS 02, ENTCS 38 (2),2002.
[105]祝义,黄志球,张广泉,周航.一种支持实时软件时间建模的形式化方法[J].解放军理工大学学报,2010,11(3)：275-276.
[106]REEDG M, ROSCOE A W. A timed model for communicating sequential processes[C]. Rennes:Proc of ICALP' 86, LNCS 226, Springer,1986.
[107]DAVIES J, SCHNEIDER S. A brief history of timed CSP [J]. Theoretical Computer Science, 1995,138(2):243-271.
[108]J. Faber, S. Jacobs, and V. S. Stokkermans. Verifying CSP-OZ-DC specification with complex Data Types and Timing Parameters. In J. Davies and J. Gibbons, editors, Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, pages 233-252. Springer-Verlag, July 2007.
[109]Object Management Group. Object constraint language version 2.0. OMG Document, format/06-05-01,2006. http://www.omg.org/cgi-bin/apps/doc?format/06-05-01.
[110]Clarke E M, Grumberg Jr O, Peled D A.Model Checking [M]. Cambridge, Massachusetts. The MIT Press.1999.
[111]J Hespanha, A. Tiwari. Fixed Point Iteration for Computing the Time Elapse Operator [C]// HSCC 2006,LNCS,2006,3927:537-551.
[112]Kuhn W. Zonotopes dynamics in numerical quality control [J]. Mathmeatical Visualization, 1998, springer,125-134.
[113]刘震.混在系统模型验证工具的验证效果分析[D].合肥：合肥工业大学.2010.
[114]K.L. Man and R.R.H. Schiffelers. Formal Specification and Analysis of Hybrid Systems [D]. PH.D Thesis of Technical University of Eindhoven.2006.
[2]徐田华.概率模型检验及其在列车运行控制系统中的应用[D].北京：北京交通大学博士后出站报告.2007.
[3]燕飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究.北京：北京交通大学博士论文,2006.
[4]员春欣.铁路信号容错技术[M].北京：中国铁道出版社,1997.
[5]王海峰.安全关键系统的形式化开发方法研究.北京：北京交通大学博士论文,2002.
[6]古天龙.软件开发的形式化方法[M].北京：高等教育出版社,2005.
[7]张曙光.京沪高速铁路系统优化研究[M].北京：中国铁道出版社,2009.
[8]丁建文,蒋文怡,钟章队GSMR移动通信网络与列车控制系统的发展[J].中国铁路,2007,(2)：46-47.
[9]J. Hoenicke, P. Maier. Model-Checking of Specification Integrating Processes, Data and Time. http://www.springerlink.com/index/98X8PV7APVDTKAGM.pdf.
[10]J.Hoenicke and E.-R.Olderog. CSP-OZ-DC:A combination of specification techniques for processed, data and time. Nordic Journal of Computing,9(4):301-334,2002. Appear March 2003.
[11]D.Craigen. Formal Methods, EVES, and Safety Critical Systems. Technical Report FR-94-5479-04[R].Minister of National Defence, Ontario, Canada,1994.
[12]Y. Papadopoulos, J.A.McDermid. The Potential for a Generic Approach to Certification of Safety Critical Systems in the Transportation Sector[J]. Reliability Engineering and Systems Safety, 1999,63(1):47-66.
[13]Neil Storey. Safety-Critical Computer Systems[M]. Addison-Wesley,1996.
[14]曹源,唐涛,徐田华,穆建成.形式化方法在列车运行控制系统中的应用[J].交通运输工程学报,2010,10(1)：114-115.
[15]CENELEC EN50129-2003. Railway applications-Communication. signalling and processing systems-Safety related electronic systems for signalling[S]. BSI.2003.
[16]IEC. IEC61508:2005. Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems[S]. IEC.2005.
[17]ERTMS Users Group. ERTMS/ETCS System Requirement Specification class1; subset-026.
[18]ERTMS Users Group. ERTMS/ETCS Function Requirement Specification FRS.
[19]李晓山,周巢尘.时段演算综述[J].计算机学报,1994,11,842-851.
[20]Chaochen Z, Hansen M. Duration Calculus-A Formal Approach to Real-Time Systems[M]. Springer-Verlag,2003.
[21]Roland Meyer. Model-Checking von Phasen-Event-Automaten bezuglich, Duration Calculus Formeln mittels Testautomaten[D]. Ph.D Thesis of UniversitAat Oldenburg, Aug 2005.
[22]A. Schafer. Combining Real-Time Model-Checking and Fault Tree Analysis. In Proc. Formal Methods Europe (FM 2003), vol.2805 of LNCS, pp.522-541. Springer,2003.
[23]R. Meyer, J. Faber, and A. Rybalchenko. Model checking duration Calculus:a practical approach. In:K. Barkaoui,A. Cavalcanti, and A. Cerone (Eds.),Proc. Int'l Coll. on Theoret.Aspects of Computing (ICTAC),vol.4281 of Lecture Notes in Computer Science, pp.332-346.Springer, 2006.
[24]S.Veloudis,N.Nissanke. Duration Calculus in the specification of safety requirement.Proceedings of the 5th International Symposim on Formal Techniques in Real-Time and Fault-Tolerant System, LCNS, vol.1486, pp.13-112,1998.
[25]Kirsten Berkenkotter Stefan Bisanz Ulrich Hannemann Jan Peleska. The HybridUML profile for UML 2.0[J]. International Journal on Software Tools for Technology (2006) 8(2):167-176
[26]Kirsten Berkenkotter Stefan Bisanz Ulrich Hannemann Jan Peleska. HybridUML profile for UML2.0. SVERTS Workshop at the UML 2003 Conference, October 2003. http://www.verimag. imag.fr/EVENTS/2003/SVERTS/.
[27]Paul Ziemann and Martin Gogolla. Validating OCL specifications with the USE tool-an example based on the BART case study. In Thomas Arts and Wan Fokkink, editors, Proc.8th Int. Workshop Formal Methods for Industrial Critical Systems (FMICS'2003), volume 80 of ENTCS. Elsevier,2003.
[28]Andr'e Platzer. Differential Dynamic Logic for Verifying Parametric Hybrid Systems[J]. Automated Reasoning with Analytic Tableaux and Related Methods, Springer Berlin/Heidelberg 2007, pp.216-232.
[29]Andr'e Platzer. A Temporal Dynamic Logic for Verifying Hybrid System Invariants[J]. Logical Foundations of Computer Science, Springer Berlin/Heidelberg 2007, pp.457-471.
[30]Andr'e Platzer, Jan-David Quesel. Logical Verification and Systematic Parametric Analysis in Train Control[J]. Lecture Notes in Computer Science[J], Springer Berlin 2008, pp.646-649.
[31]Andr'e Platzer, Jan-David Quesel. European Train Control System:A Case Study in Formal Verification [J]. Lecture Notes in Computer Science[J], Springer Berlin 2009, pp.246-265.
[32]Damm, W., Hungar, H., Olderog, E.-R.:Verification of cooperating traffic agents. International Journal of Control 79(5),395-421 (2006).
[33]Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rudiger Olderog, Jun Pang, Andre Platzer, Marc Segelken, and BorisWirtz. Automating Verification of Cooperation, Control, and Design in Traffic Applications [J]. Springer Berlin 2007, pp.115-169.
[34]Kapur D, Winter V L. On the construction of a domain language for a class of reactive systems [C]//Winter Victor L, Bhattacharya Sourav. The Kluwer International Series In Engineering And Computer Science. Massachusetts. Kluwer Academic Publishing.2001:169-196.
[35]Winter V L, Kapur D, R.S.Berg. A refinement-based approach for developing software controllers for train systems [C]//Winter Victor L, Bhattacharya Sourav. The Kluwer International Series In Engineering And Computer Science. Massachusetts. Kluwer Academic Publishing.2001:197-240.
[36]Winter V L, Kapur D,Fuehrer G. Formal specification and refinement of a safe train control function. [C]//Fsbrice Kordon Formal,Michel Lemoine.Methods for Embedded Distributed Systems:How to Master the Complexity. Massachusetts. Kluwer Academic Publishing.2004:25-64.
[37]Morten P. Lindegaard. Proof Support for RAISE[D].Kongens Lyngby. PH.D Thesis of Technical University of Denmark.2004.
[38]Meyer H M,Schnieder E. Modelling and Simulation of Train Control Systems using Petri Nets [C]//Trier University. Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Toulouse. Springer.1999:1867-1883.
[39]Jansen L,Meyer H M,Schnieder E. Technical Issues in Modelling the European Train Control Systems (ETCS) Using Coloured Petri Nets and Design/CPN Tools [R]//Aarhus Universitet. Workshop on Practical Use of Coloured Petri Nets and Design. Aarhus.1998:103-115.
[40]Michael Meyer zu Horste and Eckehard Schnieder. Modeling train control systems with Petri nets-A functional reference-architecture[C].2000 IEEE International Conference on System,man and Cybernetics. Nashville, TN, USA,2000:3081-3086.
[41]Kirsten Berkenkotter Stefan Bisanz Ulrich Hannemann Jan Peleska. Executable HybridUML and its Application to Train Control Systems.2004, LNCS 3147, pp.145-173.
[42]Paul Ziemann and Martin Gogolla. Validating OCL specifications with the USE tool-an example based on the BART case study[C]. In Thomas Arts and Wan Fokkink, editors, Proc.8th Int. Workshop Formal Methods for Industrial Critical Systems (FMICS'2003), volume 80 of ENTCS. Elsevier,2003.
[43]CONTRACT ERA/2007/ERTMS/02. ETCS tool architecture description. http://www.era.europa.eu/core/ertms/.../ETCS_architecture_v_1_0.pdf.
[44]Eckehard Schnieder, Mourad Chouikha, Stefan Einer and Michael Meyer zu Horste BASYSNET-An Integrated Approach for Automated Control System Development[C]. Petri Net Technology for Communication-Based Systems. Lecture Notes in Computer Science,2003, Volume 2472/2003,352-362.
[45]Michael Meyer zu Horste, Srinivasan Parthasarathy, Eckehard Schnieder. NOTATION,METHOD,TOOL:A CONCEPTUAL FRAMEWORK FOR THE APPLICATION OF FORMAL METHODS[C].2000 IFAC Control in Transportations Systems, braunschhweig,Germany, 2000,pp:113-118.
[46]Haxthausen A.E, Peleska J. Formal Development and Verification of a Distributed Railway Control System[J]. IEEE Transactions On Software Engineering.2000.26 (8):687-701.
[47]吕继东,唐涛,燕飞,徐田华.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证[J].铁道学报,2009,31(3)：59-64.
[48]吕继东,唐涛,贾吴.客运专线CTCS-3级列控系统无线闭塞中心的建模与验证[J].铁道学报,2010,32(6)：34-42.
[49]牛儒,曹源,唐涛ETCS-2级列控系统RBC交接协议的形式化分析[J].铁道学报,2009,31(4)：52-58.
[50]Jones CB. Systematic Software Development Using VDM.PHI Ltd1990.
[51]Splvey JM. The Z notation:A Reference Manual. Englewood Cliffs. NJ:Prentice Hall 1993.
[52]Chris George.Tutorial on the RAISE Language[C]//Method and Tools Formal Methods and Software Engineering.Berlin.Springer/Heidelberg.2004:3-4
[53]E.H. Dtlrr and J. van Katwijk. VDM++:A Formal Specification Language for Object-Oriented Designs. Computer Systems and Software Engineering, pages 214-219 IEEE Computer Society Press,1992. Proceedings of CompEuro'92.
[54]P.A. Swatman, P.M.C. Swatman, and R. Duke Electronic Data Interchange:A High-level Formal Specification in Object-Z Proceedings of 6th Australian Software Engineering Conference, pages 341-354, Sydney, Australia, Springer-Verlag,1991.
[55]K.Lano. Z++:An Object-Oriented Extension to Z. Proceedings of the 4th Annual Z user Meeting, Oxford, J.E.Nicholls(Ed.), Springer-Verlag,1001, pages 151-172.
[56]HOARE C.A.R. Communicating sequential processes [J]. Communications of the ACM.
[57]R. Gerber and I. Lee. CCSR:A Calculus for Communicating Shared Resources. In Proceedings of CONCUR'90, Lecture Notes in Computer Science, Vol.458, Springer-Verlag,1990, pages 263-277.
[58]Zhou Chaochen,WangJi and Anders P.Ravn A Formal Description of Hybrid Systems[C]. in the Proc of the DIMACS/SYCON workshop on Hybrid systems III:verification and control:verification and control Springer-Verlag New York, Inc. Secaucus, NJ, USA,1996.
[59]Claude Girault, Rudiger Valk.Petri.Nets for System Engineering-A guide to Modeling, Verification, and Applications. Springer 2003.
[60]Jensen,K. Coloured Petri Nets-Basic Concepts, Analysis Methods and Pratical Use. Volume 1 of EATCS Monographs of Theoretical Computer Science, Springer, New York.
[61]肖兵,瞿坦,王明哲.着色Petri网及其在系统建模与仿真中的应用[J].计算机工程,2001,27(1)：30-33.
[62]林闯.随机Petri网和系统性能评价[M].北京：清华大学出版社,2005.
[63]Rajeev Alur, Thao Dang, Joel M. Esposito, Rafael B. Fierro, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George J. Pappas, Oleg Sokolsky. Hierarchical Hybrid Modeling of Embedded Systems. In Proceedings of EMSOFT'2001. pp.14-31.
[64]Rajeev Alur, Radu Grosu, Yerang Hur, Vijay Kumar, Insup Lee. Modular Specification of Hybrid Systems in CHARON. In Proceedings of HSCC'2000. pp.6-19.
[65]Yerang Hur, Rafael B. Fierro, Insup Lee. Modeling Distributed Autonomous Robots Using CHARON:Formation Control Case Study. In Proceedings of ISORC'2003. pp.93-98.
[66]E. Clarke and E. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Proceedings of the Workshop on Logic of Programs. LNCS, vol. 131, pp.52-71.Springer-Verlag,1981.
[67]P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming. LNCS, vol.137,pp.337-351, Springer-Verlag, April 1982.
[68]R.Alur, C. Courcoubetis, and D.L. Dill. Model-checking in dense real-time. In formation and Computation,104:2-34,1993.
[69]G. J. Holzmann and D. Peled. The State of SPIN. In Proceedings of the 8th International Conference on Computer-Aided Verification. R. Alur and T. A.Henzinger, Eds. LNCS, vol.1102, pp. 385-389, Springer-Verlag, August 1996.
[70]Behrmann. G, Larsen. K.G, Moller. O, Divid..A, Pettersson.P and Wang Yi, UPPAAL-present and future[C]//In the Proc of the 40th IEEE Conference on Decision and Control Orlando, Florida USA, December 2001, pp.2881-2886.
[71]Goran Frehse. PHAVer:Algorithmic verification of hybrid systems past HyTech. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems:Computation and Control (HSCC'05), Mar.9-11, 2005, Zurich, CH, volume 2289 of LNCS. Springer,2005. PHAVer is available at http://www.cs.ru.nl/-goranf/.
[72]M. J. Gordon. HOL:a proof generating system for higher-order logic. In G.Biriwistle and P.anyam, editors VLSI Specification, Verification and Synthesis, pp.74-128. Kluwer Academic Publishers,1988.
[73]R.S. Boyer and J.S.Moore. A Theorem Prover for a Computational Logic.In Proceedings of the 10th International Conference on Automated Deduction, LNCS Vol.449, pp.1-15,Springer-Verlag, 1990.
[74]S. Owre, J. M. Rushby, N.Shankar and M. K. Srivas. A Tutorial on Using PVS for Hardware Verification. In Proceedings of the 2nd International Conference of Theorem Provers in Circuit Design:Theory, Practice and experience. LNCS, vol 901, pp.258-279, Springer-Verlag,1994.
[75]刘兴堂.复杂系统建模理论、方法和技术[M].北京：科学出版社,2008.
[76]刘晨.基于SEB组合框架的导弹体系对抗仿真方法研究.长沙：国防科技大学博士论文,2005.
[77]铁道部科技司CTCS-3级列控系统标准规范-客运专线CTCS-3级列控系统运营规则[M].北京：中国铁道出版社,2009.
[78]铁道部科技司CTCS-3级列控系统标准规范-CTCS-3级列控系统功能需求规范(FRS)[M].北京：中国铁道出版社,2009.
[79]铁道部科技司CTCS-3级列控系统标准规范-CTCS-3级列控系统系统需求规范(SRS)(第一册)[M].北京：中国铁道出版社,2009.
[80]铁道部科技司CTCS-3级列控系统标准规范-CTCS-3级列控系统系统需求规范(SRS)(第二册)[M].北京：中国铁道出版社,2009.
[81]铁道部科技司CTCS3级列控系统标准规范系列-CTCS-3级列控系统GSM-R网络需求规范(V1.0)[M].北京：中国铁道出版社,2008.
[82]铁道部科技司CTCS-3级列控系统标准规范系列—无线闭塞技术规范[M].北京：中国铁道出版社,2008.
[83]铁道部科技司CTCS-3级列控系统标准规范系列—-CTCS-3级列控系统应答器工程应用原则[M].北京：中国铁道出版社,2008.
[84]张曙光CTCS-3级列控系统总体技术方案[M].北京：中国铁道出版社,2008.
[85]Rumbaugh,J.etal. Object-oriented Modelling and Design. Prentice Hall, New Jersey.
[86]黄永忠等.面向对象技术与方法概论[M].北京：国防工业出版社,2002.
[87]胡军.构件化嵌入式软件设计的分析与验证.南京：南京大学博士论文,2005.
[88]刘志强.普适计算环境下基于场景的可配置服务研究[D].上海：上海交通大学博士论文,2007.
[89]Amir Pnueli. The Temporal Logic of Programs. In Proceedings of FOCS' 1977. pp.46-57.
[90]Edmund M. Clarke, Orna Grumberg, David E. Long. Model checking. In Proceedings of NATO ASI DPD'1996. pp.305-349.
[91]Clarke, E.M., Emerson, E.A., Sistla, A.P.:Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst.(1986) 244-263.
[92]Zhou Chaochen, C. A. R. Hoare, Anders P. Ravn. A Calculus of Durations. Inf. Process. Lett., 1991:269-276.
[93]Chaochen, Z., Hansen, M.R., Ravn, A.P., and Rischel, H. Duration Specifications for Shared Processors. In Proceedings of FTRTFT.1992,21-32.
[94]Chaochen, Z., Ravn, A.P., and Hansen, M.R. An Extended Duration Calculus for Hybrid Real-Time Systems. In Proceedings of Hybrid Systems.1992,36-59.
[95]Rajeev Alur, David L. Dill. A Theory of Timed Automata. Theor. Comput. Sci.,1994:183-235.
[96]Thomas A. Henzinger, The Theory of Hybrid Automata Logic in Computer Science [A]. LICS'96, Proceedings of Eleventh Annual IEEE Symposium on[C].1996.278-292.
[97]李慧芳,范玉顺.工作流系统时间管理[J].软件学报,2002,13(8)：1552-1557.
[98]冯林,姜浩.基于时间约束Petri网的工作流可调度性分析[J].计算机技术与发展,2006,16(11)：33-37.
[99]龙世荣,张广泉,汀宏海.基于时间自动机的实时工作流时序约束一致性验证[J].苏州大学学报.2009,29(6)：12-16.
[100]刘键,朱晓梅.分布式实时处理形式开发技术导论[J].计算机科学,1995,22(6)：62-73.
[101]吴瑞强.控制系统的实时性研究与优化.浙江：浙江大学博士论文,2006.
[102]李广元LTLC面向实时与混成系统的连续时序逻辑[D].北京：中国科学研究院,2001：10-11.
[103]Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, and Wang Yi. Timed Automata Patterns[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING.2008. pp.844-845.
[104]OUAKNINE J, WORRELL J. Timed CSP=Closed Timed Automata [C]. Brno:Proc of EXPRESS 02, ENTCS 38 (2),2002.
[105]祝义,黄志球,张广泉,周航.一种支持实时软件时间建模的形式化方法[J].解放军理工大学学报,2010,11(3)：275-276.
[106]REEDG M, ROSCOE A W. A timed model for communicating sequential processes[C]. Rennes:Proc of ICALP' 86, LNCS 226, Springer,1986.
[107]DAVIES J, SCHNEIDER S. A brief history of timed CSP [J]. Theoretical Computer Science, 1995,138(2):243-271.
[108]J. Faber, S. Jacobs, and V. S. Stokkermans. Verifying CSP-OZ-DC specification with complex Data Types and Timing Parameters. In J. Davies and J. Gibbons, editors, Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, pages 233-252. Springer-Verlag, July 2007.
[109]Object Management Group. Object constraint language version 2.0. OMG Document, format/06-05-01,2006. http://www.omg.org/cgi-bin/apps/doc?format/06-05-01.
[110]Clarke E M, Grumberg Jr O, Peled D A.Model Checking [M]. Cambridge, Massachusetts. The MIT Press.1999.
[111]J Hespanha, A. Tiwari. Fixed Point Iteration for Computing the Time Elapse Operator [C]// HSCC 2006,LNCS,2006,3927:537-551.
[112]Kuhn W. Zonotopes dynamics in numerical quality control [J]. Mathmeatical Visualization, 1998, springer,125-134.
[113]刘震.混在系统模型验证工具的验证效果分析[D].合肥：合肥工业大学.2010.
[114]K.L. Man and R.R.H. Schiffelers. Formal Specification and Analysis of Hybrid Systems [D]. PH.D Thesis of Technical University of Eindhoven.2006.