高速铁路列车运行控制系统的形式化建模与验证方法研究
|
摘要
高速铁路列车运行控制系统(简称：列控系统)融入了先进的计算机、通信以及控制技术,极大地提升了系统的效率和安全性。由于系统的硬件集成度不断提高,大量软件参与系统控制,使得系统特性也呈现出结构分布、实时性强、响应快速等多样化的趋势,系统特性的验证也愈加困难,因此需要找到一条更为有效、全面的方法实现列控系统的特性验证,进一步提升系统的性能或完善系统功能。基于严格数学定义的形式化方法,由于其能够精确、清晰地描述系统结构和相关特性,同时能够验证系统的相关特性,近年来在列控系统领域得到迅速发展,并且已经成为描述和验证高速铁路列控系统特性的一种重要方法。
论文对列控系统的形式化建模、描述以及验证方法的应用展开了综述。分析了RAISE (Rigorous Approach to Industrial Software Engineering,工业软件工程的严格方法)形式化方法在列控系统中建模与验证的优势,并在此基础上,首次将Timed RAISE(时间化RAISE)引入列控系统验证领域。
论文研究了基于域+Timed RAISE的高速铁路列控系统的建模和描述方法。结合高速铁路列控系统的实际特点以及复杂性,提出了一种域方法作为系统描述的切入。域方法的主要思想是将系统划分为规模较小的域模型,根据域的验证结果以及域之间的分解与组合关系,能够最终实现大系统的特性验证。
论文详细给出了域的元组、域的组合分解以及域特性的组合分解等相关定义和定理,这些定义与定理也是域方法理论体系的关键组成部分。为实现对域方法的更好说明,对典型的高速铁路列控系统—CTCS-3 (China Train Control System level 3)级列控系统进行了实际的域的划分、域模型的建立、域特性的分析、域特性的组合分解以及子域的划分,实现了对域方法理论体系的有力支撑。
论文研究了基于域+Timed RAISE的高速铁路列控系统的验证方法。对高速铁路列控系统常见的运营场景描述相关特性、系统功能以及系统性能等三类重要的域特性进行了详细分析,并给出了三类域特性中的场景交互一致性、安全功能以及实时性的定义和数学描述,并作为系统特性验证的重要依据。
论文实现了域模型与Timed RAISE结合,给出了域模型转换为TRSL (Timed RAISE Specification Language)的具体规则,同时也给出了在系统TRSL描述的证明过程中相应的推理规则和证明方法。
论文对基于域+Timed RAISE的描述和验证方法的具体应用进行了分析和举例。通过对RBC (Radio Block Center,无线闭塞中心)切换场景的交互一致性验证、等级转换(CTCS-2级至CTCS-3级)场景的实时性验证以及两车区间追踪案例中的安全功能进行了实际的域(子域)的划分、系统模型建立、Timed RAISE具体描述以及验证过程。仅为说明基于域+Timed RAISE方法的正确性,将各验证案例都进行了相应的简化和假设。最终给出了结果：列车通过RBC边界的条件下,车载设备与两个RBC的共同交互并不会带来场景交互一致性错误,即场景中各设备和子系统的交互流程是一致的；列车在等级转换(CTCS-2级至CTCS-3级)场景中,即使GSM-R (GSM for Railway)网络的通信随机延迟给场景的实时性带来了巨大的挑战,但依然能够满足场景的实时性要求；在两车追踪案例中,在给定前车以及外界的边界条件后,CTCS-3级列控系统能够在地面设备、车载设备以及GSM-R无线网络的共同作用下实现列车的安全运行。
With the extensive application of advanced computer, communication and control in high-speed railway train control systems, the efficiency and safety have been greatly improved. Because the integration density of hardware enhances and more software participate in control, many new related system characteristics have appeared, like the distributed structure, hard real-time capability, fast response and so on. So the verification of system characteristics becomes more and more difficult, and a solution which can realize the effective and across-the-board verification of high-speed railway train control system should be proposed, and make the system performance and function more improved. The formal methods based on rigorous mathematical definition have developed rapidly in the field of the train control systems, because they can accurately and clearly describe the related characteristics and structure, and verify these characteristics as well, in recent years, they have become an important way to describe and verify the high-speed railway train control system.
The formal methods of modeling, description and verification for train control system are discussed and summarized at the first. The advantages of RAISE (Rigorous Approach to Industrial Software Engineering) formal method being applied in the modeling and verification to train control system is analyzed, and on the basis of these analyses, the Timed RAISE is introduced into the verification field of train control system for the first time.
The modeling and formal description method which based on the Domain & Timed RAISE for high-speed railway train control system is studied. Combined with the actual characteristics and complexity of high-speed railway train control system, a Domain Method is proposed and this method can be a breakthrough point of system modeling. The main idea of Domain Method is that the system can be divided into small-scale domain models, in accordance with the results of domain's verification and the relation of combination and decomposition between domains, and then the characteristics verification of whole system can be realized.
The relative definitions and theorems about domain tuples, domain combination and domain characteristics are defined in detail, these definitions and theorems are the key components of theory system of Domain Method. In order to give a better illumination to Domain Method, the representative high-speed railway train control system-CTCS-3 (China Train Control System level 3) is divided into domains, and the domain models are built, the domain characteristics are analyzed, the domain characteristics are combined and decomposed and sub-domains are divided in practice, and this practical example mighty supports the theory system of Domain Method.
The verification method based on the Domain & Timed RAISE method for high-speed railway train control system is discussed. Three kind common and important domain characteristics of train control system are analyzed in detail:the relative characteristics of scene description, system function and system performance. And accurate mathematical definitions and descriptions of three specific characteristics are given, namely the scene interactive consistency, fundamental safety function and the real-time capability, these definitions and analyses serve as the important base of the verification to system characteristics.
The integration of Domain Method and Timed RAISE is achieved, the concrete transformation rules from domain models to TRSL (Timed RAISE Specification Language) are given, and the relevant reasoning rules and specific proving methods in the verification process of TRSL specification are given as well.
Some application examples of Domain & Timed RAISE method have been given. The characteristics verification of scene interactive consistency in RBC (Radio Block Center) handover scene, real-time capability in level transition (CTCS-2 to CTCS-3) scene, the safety function during trains pursuit in wayside railway is achieved, and the division of the real domains, the establishment of system models, the formal description and reasoning of Timed RAISE are analyzed and discussed in detail. To merely explain the correctness and validity of Domain & Timed RAISE method, these examples and cases have been simplified and adopt some assumptions. Finally the results are given: on the condition of one train passed the boundary between RBCs, the interactive process between onboard equipment and RBCs will not cause the errors of the scene interactive consistency; in the scene of level transition (CTCS-2 to CTCS-3), even if the uncertainty of GSM-R (GSM for Railway) wireless network is a tremendous challenge to the real-time capability, but this scene still satisfies the real-time requirements; in the case of two trains pursuit, after ascertaining the conditions of head train and the boundary of external environment, CTCS-3 can ensure the safe operation of objected train under the co-action of ground equipments, onboard equipment and GSM-R wireless network.
论文对列控系统的形式化建模、描述以及验证方法的应用展开了综述。分析了RAISE (Rigorous Approach to Industrial Software Engineering,工业软件工程的严格方法)形式化方法在列控系统中建模与验证的优势,并在此基础上,首次将Timed RAISE(时间化RAISE)引入列控系统验证领域。
论文研究了基于域+Timed RAISE的高速铁路列控系统的建模和描述方法。结合高速铁路列控系统的实际特点以及复杂性,提出了一种域方法作为系统描述的切入。域方法的主要思想是将系统划分为规模较小的域模型,根据域的验证结果以及域之间的分解与组合关系,能够最终实现大系统的特性验证。
论文详细给出了域的元组、域的组合分解以及域特性的组合分解等相关定义和定理,这些定义与定理也是域方法理论体系的关键组成部分。为实现对域方法的更好说明,对典型的高速铁路列控系统—CTCS-3 (China Train Control System level 3)级列控系统进行了实际的域的划分、域模型的建立、域特性的分析、域特性的组合分解以及子域的划分,实现了对域方法理论体系的有力支撑。
论文研究了基于域+Timed RAISE的高速铁路列控系统的验证方法。对高速铁路列控系统常见的运营场景描述相关特性、系统功能以及系统性能等三类重要的域特性进行了详细分析,并给出了三类域特性中的场景交互一致性、安全功能以及实时性的定义和数学描述,并作为系统特性验证的重要依据。
论文实现了域模型与Timed RAISE结合,给出了域模型转换为TRSL (Timed RAISE Specification Language)的具体规则,同时也给出了在系统TRSL描述的证明过程中相应的推理规则和证明方法。
论文对基于域+Timed RAISE的描述和验证方法的具体应用进行了分析和举例。通过对RBC (Radio Block Center,无线闭塞中心)切换场景的交互一致性验证、等级转换(CTCS-2级至CTCS-3级)场景的实时性验证以及两车区间追踪案例中的安全功能进行了实际的域(子域)的划分、系统模型建立、Timed RAISE具体描述以及验证过程。仅为说明基于域+Timed RAISE方法的正确性,将各验证案例都进行了相应的简化和假设。最终给出了结果：列车通过RBC边界的条件下,车载设备与两个RBC的共同交互并不会带来场景交互一致性错误,即场景中各设备和子系统的交互流程是一致的；列车在等级转换(CTCS-2级至CTCS-3级)场景中,即使GSM-R (GSM for Railway)网络的通信随机延迟给场景的实时性带来了巨大的挑战,但依然能够满足场景的实时性要求；在两车追踪案例中,在给定前车以及外界的边界条件后,CTCS-3级列控系统能够在地面设备、车载设备以及GSM-R无线网络的共同作用下实现列车的安全运行。
With the extensive application of advanced computer, communication and control in high-speed railway train control systems, the efficiency and safety have been greatly improved. Because the integration density of hardware enhances and more software participate in control, many new related system characteristics have appeared, like the distributed structure, hard real-time capability, fast response and so on. So the verification of system characteristics becomes more and more difficult, and a solution which can realize the effective and across-the-board verification of high-speed railway train control system should be proposed, and make the system performance and function more improved. The formal methods based on rigorous mathematical definition have developed rapidly in the field of the train control systems, because they can accurately and clearly describe the related characteristics and structure, and verify these characteristics as well, in recent years, they have become an important way to describe and verify the high-speed railway train control system.
The formal methods of modeling, description and verification for train control system are discussed and summarized at the first. The advantages of RAISE (Rigorous Approach to Industrial Software Engineering) formal method being applied in the modeling and verification to train control system is analyzed, and on the basis of these analyses, the Timed RAISE is introduced into the verification field of train control system for the first time.
The modeling and formal description method which based on the Domain & Timed RAISE for high-speed railway train control system is studied. Combined with the actual characteristics and complexity of high-speed railway train control system, a Domain Method is proposed and this method can be a breakthrough point of system modeling. The main idea of Domain Method is that the system can be divided into small-scale domain models, in accordance with the results of domain's verification and the relation of combination and decomposition between domains, and then the characteristics verification of whole system can be realized.
The relative definitions and theorems about domain tuples, domain combination and domain characteristics are defined in detail, these definitions and theorems are the key components of theory system of Domain Method. In order to give a better illumination to Domain Method, the representative high-speed railway train control system-CTCS-3 (China Train Control System level 3) is divided into domains, and the domain models are built, the domain characteristics are analyzed, the domain characteristics are combined and decomposed and sub-domains are divided in practice, and this practical example mighty supports the theory system of Domain Method.
The verification method based on the Domain & Timed RAISE method for high-speed railway train control system is discussed. Three kind common and important domain characteristics of train control system are analyzed in detail:the relative characteristics of scene description, system function and system performance. And accurate mathematical definitions and descriptions of three specific characteristics are given, namely the scene interactive consistency, fundamental safety function and the real-time capability, these definitions and analyses serve as the important base of the verification to system characteristics.
The integration of Domain Method and Timed RAISE is achieved, the concrete transformation rules from domain models to TRSL (Timed RAISE Specification Language) are given, and the relevant reasoning rules and specific proving methods in the verification process of TRSL specification are given as well.
Some application examples of Domain & Timed RAISE method have been given. The characteristics verification of scene interactive consistency in RBC (Radio Block Center) handover scene, real-time capability in level transition (CTCS-2 to CTCS-3) scene, the safety function during trains pursuit in wayside railway is achieved, and the division of the real domains, the establishment of system models, the formal description and reasoning of Timed RAISE are analyzed and discussed in detail. To merely explain the correctness and validity of Domain & Timed RAISE method, these examples and cases have been simplified and adopt some assumptions. Finally the results are given: on the condition of one train passed the boundary between RBCs, the interactive process between onboard equipment and RBCs will not cause the errors of the scene interactive consistency; in the scene of level transition (CTCS-2 to CTCS-3), even if the uncertainty of GSM-R (GSM for Railway) wireless network is a tremendous challenge to the real-time capability, but this scene still satisfies the real-time requirements; in the case of two trains pursuit, after ascertaining the conditions of head train and the boundary of external environment, CTCS-3 can ensure the safe operation of objected train under the co-action of ground equipments, onboard equipment and GSM-R wireless network.
引文
[1]张曙光.京沪高速铁路系统优化研究[M].北京.中国铁道出版社.2009.
[2]张曙光.铁路高速列车应用基础理论与工程技术[M].北京.科学出版社.2007.
[3]张曙光CTCS-3级列控系统总体技术方案[M].北京.中国铁道出版社.2008.
[4]黎忠文,陈亮,熊光泽.基于防危核(壳)的安全关键硬实时系统响应时间的分析[J].电子学报.2006.34(4)：647-652.
[5]谭良,周明天.大型复杂软件系统安全需求的体系结构模型[J].计算机科学.2007.34(12)：266-277.
[6]汪希时.智能铁路运输系统ITS-R[M].北京.中国铁道出版社.2004.
[7]张曙光.高速铁路系统生命周期安全评估体系的研究[J].铁道学报2007.29(2)：20-26.
[8]燕飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D].北京.北京交通大学博士论文.2006.
[9]吴芳美.铁路安全软件测试评估[M].北京.中国铁道出版社.2001.
[10]IEC. IEC61508:2005. Functional Safety of Electrical/Electronic/Programmable Electronic Safety—Related Systems[S]. IEC.2005.
[11]唐涛,徐田华,赵林.列车运行控制系统规范建模与验证[M].北京.中国铁道出版社.2010.
[12]Edmund M.Clarke, Jr.Orna Grumberg and Doron A.Peled. Model Checking[M]. Massachusetts. The MIT Press Cambridge.1999.
[13]徐田华.概率模型检验及其在列车运行控制系统中的应用[D].北京.北京交通大学博士后出站报告.2007.
[14]王海峰,陈建明,张仲义.安全苛求系统的形式化开发方法[J].北方交通大学学报.2002.26(6)：52-55.
[15]IEC. IEC62425:2007. Railway Applications-Communication, Signaling and Processing Systems-Safety Related Electronic Systems for Signaling[S]. IEC.2003.
[16]IEC. IEC62279:2002. Railway Applications-Communications, Signalling and Processing Systems-Software for Railway Control and Protection Systems[S]. IEC.2001.
[17]维基百科—形式化的定义[R].http://zh.wikipedia.org/wiki/%E5%BD%A2%E5%BC% 8F%E5%8C%96%E6%96%B9%E6%B3%95.
[18]J. R. Abrial. Formal Methods in Industry:Achievements, Problems, Future//ACM.28th International Conference on Software Engineering(ICSE 2006). Shanghai. ACM.2006:761-767.
[19]肖健宇,张德运,陈海诠,董浩.模型检测与定理证明相结合开发并验证高可信嵌入式软件[J].吉林大学学报(工学版).2005.35(5)：531-537.
[20]杨军,葛海通,郑飞君,严晓浪.一种形式化验证方法：模型检验[J].浙江大学学报(理学版).2006.33(7)：403-407.
[21]古天龙.软件开发的形式化方法[M].北京.高等教育出版社.2005.
[22]郑红军,张乃孝.软件开发中的形式化方法[J].计算机科学.1997.24(6)：90-96.
[23]Armin Z, Gunter H. A train Control System Case Study in Model-based Real-time System Design [C]//IEEE. Proceedings of the 17th International Symposium on Parallel and Distributed Processing. Washington. IEEE.2003:118-126.
[24]Armin Z, Gunter H. Towards Modeling and Evaluation of ETCS Real-time Communication and Operation[J]. The Journal of Systems and Software.2005.77 (1):47-54.
[25]林闯.随机Petri网和系统性能评价[M].北京.清华大学出版社.2005.
[26]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.
[27]Jansen L, Meyer H M, Schnieder E. Technical Issues in Modelling the European Train Control System (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.
[28]Einer S, Slovak R, Schnieder E. Modeling train control systems with Petrinets-an operational specification[C]//IEEE. International Conference on Systems, Man, and Cybernetics. Tennessee. IEEE.2000:3207-3211.
[29]肖兵,瞿坦,王明哲.着色Petri网及其在系统建模与仿真中的应用[J].计算机工程.2001.27(1)：30-33.
[30]Johannes F, Swen J, Viorica S S. Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters[C]//University of Oxford. Integrated Formal Methods. Oxford. University of Oxford.2007:233-252.
[31]Ernst-Rudiger O. Automatic Verification of Combined Specifications[J]. An Overview Electronic Notes in Theoretical Computer Science.2008.207:3-16.
[32]AVACS S3. A Fault Tree Based Model for ETCS Application Level 2[R]. Bonn. AVACS.2007.
[33]AVACS S3. Brake Risk Assessment for ETCS Train Platoons[R]. Bonn. AVACS.2007.
[34]Roland M. Model-Checking von Phasen-Event-Automaten bezuglich, Duration Calculus Formeln mittels Testautomaten[D]. Oldenburg. UniversitAat Oldenburg.2005.
[35]Meyer R, Faber J, Hoenicke J, et al. Model Checking Duration Calculus:a practical approach[J]. Formal Aspect s of Computing.2008.20(4):481-505.
[36]Faber J. Verifying Real-time Aspects of the European Train Control System[C]//University of Copenhagen. Proceedings of the 17th Nordic Workshop on Programming Theory. Copenhagen. DIKU.2005:67-70.
[37]Tapken J. Model-checking of Duration Calculus Specifications[D]. Oldenburg. University Oldenburg.2001.
[38]Andr'e P. Differential Dynamic Logic for Verifying Parametric Hybrid Systems[C]//Automated Reasoning with Analytic Tableaux and Related Methods. Aixen Provence. Springer Berlin/Heidelberg.2007:216-232.
[39]Andr'e P. A Temporal. A Temporal Dynamic Logic for Verifying Hybrid System Invariants[C]// Logical Foundations of Computer Science. New York. Springer Berlin/Heidelberg. 2007:457-471.
[40]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.
[41]Morten M. Modelling a Distributed Railway Control System[D]. Kongens Lyngby. Master Thesis of Technical University of Denmark.2005.
[42]Haxthausen A.E, Peleska J. A Distributed Railway Control System Selected Proofs.http:// www.it.dtu.dk/～ah/Dracos.2000.
[43]李黎.混成系统的描述和设计与Timed RAISE项目[J].计算机科学.2001.27(7)：82-84.
[44]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.
[45]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.
[46]Winter V L, Kapur D, Fuehrer G. Formal specification and refinement of a safe train control function. [C]//Fabrice Kordon Formal, Michel Lemoine. Methods for Embedded Distributed Systems:How to Master the Complexity. Massachusetts. Kluwer Academic Publishing. 2004:25-64.
[47]B. Dandanell, J. Gφrtz, J. Storbank Pedersen and E. Zierau. Experiences from Applications of RAISE[C]//FME'93:Industrial-Strength Formal Methods. Berlin. Springer/Heidelberg. 1993:52-63.
[48]D. Bjφrner, A. Haxthausen and K. Havelund. Formal, Model-oriented Software Development Methods - From VDM to ProCoS & from RAISE to LaCoS[J]. Future Generation Computer Systems.1992(7):111-138.
[49]Chris George. Tutorial on the RAISE Language[C]//Method and Tools Formal Methods and Software Engineering. Berlin. Springer/Heidelberg.2004:3-4.
[50]PRaCoSy:Document Deliverables[R]. http://www.iist.unu.edu/newrh/Ⅱ/1/2/1/ docs/page.html
[51]The RAISE Method Group. The RAISE Development Method[M]. N.J. Prentice Hall Int.1995.
[52]C. A. R. Hoare. Communicating Sequential Processes[M]. N.J. Prentice Hall International.1985.
[53]陈怡海,缪淮扣.两种形式语言：RSL与Z的分析比较[J].计算机应用与软件.2002.19(4)：11-50.
[54]贾若宇,赵保华,屈玉贵,顾翔.CSP和RSL应用于协议形式化描述的研究[J].计算机应用.2003.23(1)：10-13.
[55]顾翔.基于RSL的协议形式化描述语言研究[D].合肥.中国科学技术大学.2004.
[56]顾翔,邱建林,蒋峥峥.RSL在协议形式化描述中的应用研究[J].计算机应用.2007.27(9)：2236-2238.
[57]Morten P. Lindegaard. Proof Support for RAISE[D]. Kongens Lyngby. PH.D Thesis of Technical University of Denmark.2004.
[58]Xia Yong, Chris George. An operational semantics for timed RAISE[C]//FM'99—Formal Methods. Springer Berlin/Heidelberg.1999:715-734.
[59]Ri Hyon Sul, He Jifeng. A Complete Verification System for Timed RSL (2003) [R]. No.275. Report of United Nations University (UNU).2003.
[60]Li li, He Jifeng. A Denotational Semantics of Timed RSL Using Duration Calculus[J]软件学报.2001.12(6)：802-816.
[61]Haxthausen A. E, Xia Yong. Linking DC Together with TRSL[C]//Integrated Formal Methods: Second International Conference(IFM 2000). Dagstuhl Castle. Springer Berlin/Heidelberg. 2000:25-44.
[62]LI Li. Towards a Denotational Semantics of Timed RSL Using Duration Calculus[J]. Journal of Computer Science & Technology.2001.16 (1):64-76.
[63]John J Marciniak. Encyclopedia of Software Engineering(2nd Edition) [M]. New York. SetWiley-Interscience.2002.
[64]Graeme Smith. The Object-Z Specification Language(Advances in Formal Methods) [M]. Netherlands. Kluwer Academic Publishing.1999.
[65]李晓山,周巢尘.时段演算综述[J].计算机学报.1994.16(11)：842-851.
[66]Herbert B. Enderton. A Mathematical Introduction to Logic(Second Edition) [M]. San Diego. Academic Press.2001.
[67]Stephen R Schach. Object-Oriented and Classical Software Engineering(The 6th edition) [M]. New York. McGrawHill.2004.
[68]C. George, A. E. Haxthausen. The Logic of the RAISE Specification Language[J]. Computing and Informatics.2003.20 (1):1-27.
[69]谢兄,张维石.构件适应和组装的形式化语义描述[J].计算机工程与应用.2007.43(21)：36-39.
[70]谢兄,张维石.一种基于线性逻辑的构件组装方法研究[J].小型微型计算机系统.2008.29(5)：797-800.
[71]杨亚伟.面向本质特征的特定领域建模及其在铁路中的应用[D].铁道科学院博士学位论文.2006.
[72]胡军,于笑丰,张岩,王林章,李宣东.基于场景规约的构件式系统设计分析与验证[J].计算机学报.2006.29(4)：513-525.
[73]卓琳,刘万伟,谭庆平.基于场景的性质验证方法[J].计算机工程与科学.2006.28(4)：56-59.
[74]郑宇恒.一种基于场景的需求验证方法[J].计算机时代.2008.11：4-7.
[75]张曙光.京津城际铁路系统调试技术[M].北京.中国铁道出版社.2008.
[76]中国铁道科学研究院.武广客运专线联调联试及运行试验总报告(V2.0)[R].北京.TY字第2638-2号.2009.
[77]燕飞,唐涛.轨道交通信号系统安全技术的发展和研究现状[J].中国安全科学学报.2005.15(6)：94-99.
[78]熊光泽,常政威,桑楠.可信计算发展综述[J].计算机应用.2009.29(4)：915-919.
[79]Eddie Goddard. Electric Traction Systems Overview of Signalling and Train Control Systems[J]. Electric Traction Systems.2008.11:314-322.
[80]铁道部科技司CTCS-3级列控系统标准规范—客运专线CTCS-3级列控系统运营规则[M].北京.中国铁道出版社.2009.
[81]铁道部科技司CTCS-3级列控系统标准规范—CTCS-3级列控系统系统功能需求规范(FRS)[M].北京.中国铁道出版社.2009.
[82]铁道部科技司CTCS-3级列控系统标准规范—CTCS-3级列控系统系统需求规范(SRS)(第一册)[M].北京.中国铁道出版社.2009.
[83]铁道部科技司CTCS-3级列控系统标准规范—CTCS-3级列控系统系统需求规范(SRS)(第二册)[M].北京.中国铁道出版社.2009.
[84]杨仕平,熊光泽,桑楠.安全关键系统高可信保障技术的研究[J].计算机科学.2003. 30(5)：97-101.
[85]黎忠文.分布式控制系统中新安全保障技术的研究—安全核技术[D].电子科技大学博士学位论文.2001.
[86]杨仕平,熊光泽,桑楠.安全关键系统的防危性技术研究[J].电子科技大学学报.2003.32(4)：164-169.
[87]Winter V L, Kapur D, Fuehrer G Towards Dynamic Partitioning of Reactive System Behavior: A Train Controller Case Study[C]//Fabrice Kordon, Janos Sztipanovits. Reliable Systems on Unreliable Networked Platforms. Berlin. Springer.2007:47-69.
[88]Tianhua Xu, Tao Tang, Chunhai Gao, Baigen Cai. Logic verification of Collision Avoidance System in train control systems[C]//IEEE. Intelligent Vehicles Symposium 2009. Xi'an. IEEE. 2009:918-923.
[89]铁道部科技司CTCS-3级列控系统标准规范系列—CTCS-3级列控系统GSM-R网络需求规范(V1.0)[M].北京.中国铁道出版社.2008.
[90]C. George, S. Prehn. The RAISE Justification Handbook[M]. LACOS/CRI/DOC/7/V5.1994
[91]The RAISE Method Group. The RAISE Specification Language[M]. N.J. Series. Prentice Hall Int.1992.
[92]牛儒,曹源,唐涛.ETCS-2级列控系统RBC交接协议的形式化分析[J].铁道学报.2009.31(4)：52-58.
[93]Uhlirz. M. Concept of a GSM-based communication system for high-speed trains[C]//IEEE. 44th Vehicular Technology Conference. IEEE. Stockholm.1994:1130-1134.
[94]Shangguan Wei, Cai Baigen, Wang Jian. Research of MRM-based CTCS-3 level train operation control system simulation support technology[C]//IEEE. Asia-Pacific Conference on Information Processing (APCIP 2009). Shenzhen. IEEE.2009:418-421.
[95]铁道部科技司CTCS-3级列控系统标准规范—无线闭塞中心技术规范[M].北京.中国铁道出版社.2008.
[96]铁道部科技司CTCS-3级列控系统标准规范—CTCS-3级列控系统应答器工程应用原则[M].北京.中国铁道出版社.2008.
[97]吕继东,唐涛,燕飞,徐天华.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证[J].铁道学报.2009.31(3)：59-64.
[98]郜春海,唐涛,张建明.高速铁路列车运行控制系统车载设备的软件设计[J].北方交通大学学报.1999.23(5)：77-82.
[99]K. Mark Hansen. Formalizing Railway Interlocking Systems[M]. Proc. Second FME Rail Workshop.1998.
[100]黄卫中,季学胜,刘岭CTCS-3级列控车载设备高速适应性关键技术[J].中国铁道科学.2010.31(3)：87-92.
[101]徐啸明.列控车载设备(CTCS2-200H型)[M].北京.中国铁道出版社.2007.
[102]王化深,王俊峰.200-350 km/h列车运行控制系统关键技术研究[J].铁道学报.2009.31(3)：107-110.
[103]蔡伯根,上官伟,李小琴,王剑.基于多分辨率建模的CTCS-3级列控系统仿真支撑技术[J].北京交通大学学报.2010.34(2)：5-10.
[2]张曙光.铁路高速列车应用基础理论与工程技术[M].北京.科学出版社.2007.
[3]张曙光CTCS-3级列控系统总体技术方案[M].北京.中国铁道出版社.2008.
[4]黎忠文,陈亮,熊光泽.基于防危核(壳)的安全关键硬实时系统响应时间的分析[J].电子学报.2006.34(4)：647-652.
[5]谭良,周明天.大型复杂软件系统安全需求的体系结构模型[J].计算机科学.2007.34(12)：266-277.
[6]汪希时.智能铁路运输系统ITS-R[M].北京.中国铁道出版社.2004.
[7]张曙光.高速铁路系统生命周期安全评估体系的研究[J].铁道学报2007.29(2)：20-26.
[8]燕飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D].北京.北京交通大学博士论文.2006.
[9]吴芳美.铁路安全软件测试评估[M].北京.中国铁道出版社.2001.
[10]IEC. IEC61508:2005. Functional Safety of Electrical/Electronic/Programmable Electronic Safety—Related Systems[S]. IEC.2005.
[11]唐涛,徐田华,赵林.列车运行控制系统规范建模与验证[M].北京.中国铁道出版社.2010.
[12]Edmund M.Clarke, Jr.Orna Grumberg and Doron A.Peled. Model Checking[M]. Massachusetts. The MIT Press Cambridge.1999.
[13]徐田华.概率模型检验及其在列车运行控制系统中的应用[D].北京.北京交通大学博士后出站报告.2007.
[14]王海峰,陈建明,张仲义.安全苛求系统的形式化开发方法[J].北方交通大学学报.2002.26(6)：52-55.
[15]IEC. IEC62425:2007. Railway Applications-Communication, Signaling and Processing Systems-Safety Related Electronic Systems for Signaling[S]. IEC.2003.
[16]IEC. IEC62279:2002. Railway Applications-Communications, Signalling and Processing Systems-Software for Railway Control and Protection Systems[S]. IEC.2001.
[17]维基百科—形式化的定义[R].http://zh.wikipedia.org/wiki/%E5%BD%A2%E5%BC% 8F%E5%8C%96%E6%96%B9%E6%B3%95.
[18]J. R. Abrial. Formal Methods in Industry:Achievements, Problems, Future//ACM.28th International Conference on Software Engineering(ICSE 2006). Shanghai. ACM.2006:761-767.
[19]肖健宇,张德运,陈海诠,董浩.模型检测与定理证明相结合开发并验证高可信嵌入式软件[J].吉林大学学报(工学版).2005.35(5)：531-537.
[20]杨军,葛海通,郑飞君,严晓浪.一种形式化验证方法：模型检验[J].浙江大学学报(理学版).2006.33(7)：403-407.
[21]古天龙.软件开发的形式化方法[M].北京.高等教育出版社.2005.
[22]郑红军,张乃孝.软件开发中的形式化方法[J].计算机科学.1997.24(6)：90-96.
[23]Armin Z, Gunter H. A train Control System Case Study in Model-based Real-time System Design [C]//IEEE. Proceedings of the 17th International Symposium on Parallel and Distributed Processing. Washington. IEEE.2003:118-126.
[24]Armin Z, Gunter H. Towards Modeling and Evaluation of ETCS Real-time Communication and Operation[J]. The Journal of Systems and Software.2005.77 (1):47-54.
[25]林闯.随机Petri网和系统性能评价[M].北京.清华大学出版社.2005.
[26]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.
[27]Jansen L, Meyer H M, Schnieder E. Technical Issues in Modelling the European Train Control System (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.
[28]Einer S, Slovak R, Schnieder E. Modeling train control systems with Petrinets-an operational specification[C]//IEEE. International Conference on Systems, Man, and Cybernetics. Tennessee. IEEE.2000:3207-3211.
[29]肖兵,瞿坦,王明哲.着色Petri网及其在系统建模与仿真中的应用[J].计算机工程.2001.27(1)：30-33.
[30]Johannes F, Swen J, Viorica S S. Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters[C]//University of Oxford. Integrated Formal Methods. Oxford. University of Oxford.2007:233-252.
[31]Ernst-Rudiger O. Automatic Verification of Combined Specifications[J]. An Overview Electronic Notes in Theoretical Computer Science.2008.207:3-16.
[32]AVACS S3. A Fault Tree Based Model for ETCS Application Level 2[R]. Bonn. AVACS.2007.
[33]AVACS S3. Brake Risk Assessment for ETCS Train Platoons[R]. Bonn. AVACS.2007.
[34]Roland M. Model-Checking von Phasen-Event-Automaten bezuglich, Duration Calculus Formeln mittels Testautomaten[D]. Oldenburg. UniversitAat Oldenburg.2005.
[35]Meyer R, Faber J, Hoenicke J, et al. Model Checking Duration Calculus:a practical approach[J]. Formal Aspect s of Computing.2008.20(4):481-505.
[36]Faber J. Verifying Real-time Aspects of the European Train Control System[C]//University of Copenhagen. Proceedings of the 17th Nordic Workshop on Programming Theory. Copenhagen. DIKU.2005:67-70.
[37]Tapken J. Model-checking of Duration Calculus Specifications[D]. Oldenburg. University Oldenburg.2001.
[38]Andr'e P. Differential Dynamic Logic for Verifying Parametric Hybrid Systems[C]//Automated Reasoning with Analytic Tableaux and Related Methods. Aixen Provence. Springer Berlin/Heidelberg.2007:216-232.
[39]Andr'e P. A Temporal. A Temporal Dynamic Logic for Verifying Hybrid System Invariants[C]// Logical Foundations of Computer Science. New York. Springer Berlin/Heidelberg. 2007:457-471.
[40]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.
[41]Morten M. Modelling a Distributed Railway Control System[D]. Kongens Lyngby. Master Thesis of Technical University of Denmark.2005.
[42]Haxthausen A.E, Peleska J. A Distributed Railway Control System Selected Proofs.http:// www.it.dtu.dk/～ah/Dracos.2000.
[43]李黎.混成系统的描述和设计与Timed RAISE项目[J].计算机科学.2001.27(7)：82-84.
[44]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.
[45]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.
[46]Winter V L, Kapur D, Fuehrer G. Formal specification and refinement of a safe train control function. [C]//Fabrice Kordon Formal, Michel Lemoine. Methods for Embedded Distributed Systems:How to Master the Complexity. Massachusetts. Kluwer Academic Publishing. 2004:25-64.
[47]B. Dandanell, J. Gφrtz, J. Storbank Pedersen and E. Zierau. Experiences from Applications of RAISE[C]//FME'93:Industrial-Strength Formal Methods. Berlin. Springer/Heidelberg. 1993:52-63.
[48]D. Bjφrner, A. Haxthausen and K. Havelund. Formal, Model-oriented Software Development Methods - From VDM to ProCoS & from RAISE to LaCoS[J]. Future Generation Computer Systems.1992(7):111-138.
[49]Chris George. Tutorial on the RAISE Language[C]//Method and Tools Formal Methods and Software Engineering. Berlin. Springer/Heidelberg.2004:3-4.
[50]PRaCoSy:Document Deliverables[R]. http://www.iist.unu.edu/newrh/Ⅱ/1/2/1/ docs/page.html
[51]The RAISE Method Group. The RAISE Development Method[M]. N.J. Prentice Hall Int.1995.
[52]C. A. R. Hoare. Communicating Sequential Processes[M]. N.J. Prentice Hall International.1985.
[53]陈怡海,缪淮扣.两种形式语言：RSL与Z的分析比较[J].计算机应用与软件.2002.19(4)：11-50.
[54]贾若宇,赵保华,屈玉贵,顾翔.CSP和RSL应用于协议形式化描述的研究[J].计算机应用.2003.23(1)：10-13.
[55]顾翔.基于RSL的协议形式化描述语言研究[D].合肥.中国科学技术大学.2004.
[56]顾翔,邱建林,蒋峥峥.RSL在协议形式化描述中的应用研究[J].计算机应用.2007.27(9)：2236-2238.
[57]Morten P. Lindegaard. Proof Support for RAISE[D]. Kongens Lyngby. PH.D Thesis of Technical University of Denmark.2004.
[58]Xia Yong, Chris George. An operational semantics for timed RAISE[C]//FM'99—Formal Methods. Springer Berlin/Heidelberg.1999:715-734.
[59]Ri Hyon Sul, He Jifeng. A Complete Verification System for Timed RSL (2003) [R]. No.275. Report of United Nations University (UNU).2003.
[60]Li li, He Jifeng. A Denotational Semantics of Timed RSL Using Duration Calculus[J]软件学报.2001.12(6)：802-816.
[61]Haxthausen A. E, Xia Yong. Linking DC Together with TRSL[C]//Integrated Formal Methods: Second International Conference(IFM 2000). Dagstuhl Castle. Springer Berlin/Heidelberg. 2000:25-44.
[62]LI Li. Towards a Denotational Semantics of Timed RSL Using Duration Calculus[J]. Journal of Computer Science & Technology.2001.16 (1):64-76.
[63]John J Marciniak. Encyclopedia of Software Engineering(2nd Edition) [M]. New York. SetWiley-Interscience.2002.
[64]Graeme Smith. The Object-Z Specification Language(Advances in Formal Methods) [M]. Netherlands. Kluwer Academic Publishing.1999.
[65]李晓山,周巢尘.时段演算综述[J].计算机学报.1994.16(11)：842-851.
[66]Herbert B. Enderton. A Mathematical Introduction to Logic(Second Edition) [M]. San Diego. Academic Press.2001.
[67]Stephen R Schach. Object-Oriented and Classical Software Engineering(The 6th edition) [M]. New York. McGrawHill.2004.
[68]C. George, A. E. Haxthausen. The Logic of the RAISE Specification Language[J]. Computing and Informatics.2003.20 (1):1-27.
[69]谢兄,张维石.构件适应和组装的形式化语义描述[J].计算机工程与应用.2007.43(21)：36-39.
[70]谢兄,张维石.一种基于线性逻辑的构件组装方法研究[J].小型微型计算机系统.2008.29(5)：797-800.
[71]杨亚伟.面向本质特征的特定领域建模及其在铁路中的应用[D].铁道科学院博士学位论文.2006.
[72]胡军,于笑丰,张岩,王林章,李宣东.基于场景规约的构件式系统设计分析与验证[J].计算机学报.2006.29(4)：513-525.
[73]卓琳,刘万伟,谭庆平.基于场景的性质验证方法[J].计算机工程与科学.2006.28(4)：56-59.
[74]郑宇恒.一种基于场景的需求验证方法[J].计算机时代.2008.11：4-7.
[75]张曙光.京津城际铁路系统调试技术[M].北京.中国铁道出版社.2008.
[76]中国铁道科学研究院.武广客运专线联调联试及运行试验总报告(V2.0)[R].北京.TY字第2638-2号.2009.
[77]燕飞,唐涛.轨道交通信号系统安全技术的发展和研究现状[J].中国安全科学学报.2005.15(6)：94-99.
[78]熊光泽,常政威,桑楠.可信计算发展综述[J].计算机应用.2009.29(4)：915-919.
[79]Eddie Goddard. Electric Traction Systems Overview of Signalling and Train Control Systems[J]. Electric Traction Systems.2008.11:314-322.
[80]铁道部科技司CTCS-3级列控系统标准规范—客运专线CTCS-3级列控系统运营规则[M].北京.中国铁道出版社.2009.
[81]铁道部科技司CTCS-3级列控系统标准规范—CTCS-3级列控系统系统功能需求规范(FRS)[M].北京.中国铁道出版社.2009.
[82]铁道部科技司CTCS-3级列控系统标准规范—CTCS-3级列控系统系统需求规范(SRS)(第一册)[M].北京.中国铁道出版社.2009.
[83]铁道部科技司CTCS-3级列控系统标准规范—CTCS-3级列控系统系统需求规范(SRS)(第二册)[M].北京.中国铁道出版社.2009.
[84]杨仕平,熊光泽,桑楠.安全关键系统高可信保障技术的研究[J].计算机科学.2003. 30(5)：97-101.
[85]黎忠文.分布式控制系统中新安全保障技术的研究—安全核技术[D].电子科技大学博士学位论文.2001.
[86]杨仕平,熊光泽,桑楠.安全关键系统的防危性技术研究[J].电子科技大学学报.2003.32(4)：164-169.
[87]Winter V L, Kapur D, Fuehrer G Towards Dynamic Partitioning of Reactive System Behavior: A Train Controller Case Study[C]//Fabrice Kordon, Janos Sztipanovits. Reliable Systems on Unreliable Networked Platforms. Berlin. Springer.2007:47-69.
[88]Tianhua Xu, Tao Tang, Chunhai Gao, Baigen Cai. Logic verification of Collision Avoidance System in train control systems[C]//IEEE. Intelligent Vehicles Symposium 2009. Xi'an. IEEE. 2009:918-923.
[89]铁道部科技司CTCS-3级列控系统标准规范系列—CTCS-3级列控系统GSM-R网络需求规范(V1.0)[M].北京.中国铁道出版社.2008.
[90]C. George, S. Prehn. The RAISE Justification Handbook[M]. LACOS/CRI/DOC/7/V5.1994
[91]The RAISE Method Group. The RAISE Specification Language[M]. N.J. Series. Prentice Hall Int.1992.
[92]牛儒,曹源,唐涛.ETCS-2级列控系统RBC交接协议的形式化分析[J].铁道学报.2009.31(4)：52-58.
[93]Uhlirz. M. Concept of a GSM-based communication system for high-speed trains[C]//IEEE. 44th Vehicular Technology Conference. IEEE. Stockholm.1994:1130-1134.
[94]Shangguan Wei, Cai Baigen, Wang Jian. Research of MRM-based CTCS-3 level train operation control system simulation support technology[C]//IEEE. Asia-Pacific Conference on Information Processing (APCIP 2009). Shenzhen. IEEE.2009:418-421.
[95]铁道部科技司CTCS-3级列控系统标准规范—无线闭塞中心技术规范[M].北京.中国铁道出版社.2008.
[96]铁道部科技司CTCS-3级列控系统标准规范—CTCS-3级列控系统应答器工程应用原则[M].北京.中国铁道出版社.2008.
[97]吕继东,唐涛,燕飞,徐天华.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证[J].铁道学报.2009.31(3)：59-64.
[98]郜春海,唐涛,张建明.高速铁路列车运行控制系统车载设备的软件设计[J].北方交通大学学报.1999.23(5)：77-82.
[99]K. Mark Hansen. Formalizing Railway Interlocking Systems[M]. Proc. Second FME Rail Workshop.1998.
[100]黄卫中,季学胜,刘岭CTCS-3级列控车载设备高速适应性关键技术[J].中国铁道科学.2010.31(3)：87-92.
[101]徐啸明.列控车载设备(CTCS2-200H型)[M].北京.中国铁道出版社.2007.
[102]王化深,王俊峰.200-350 km/h列车运行控制系统关键技术研究[J].铁道学报.2009.31(3)：107-110.
[103]蔡伯根,上官伟,李小琴,王剑.基于多分辨率建模的CTCS-3级列控系统仿真支撑技术[J].北京交通大学学报.2010.34(2)：5-10.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |