列车通信网络系统形式化建模与验证方法研究
|
摘要
随着现场总线技术、计算机网络通信技术、嵌入式系统控制技术以及故障诊断技术的快速发展,现代列车控制系统已经从孤立的数字控制系统发展成为基于网络的分布式控制系统。列车通信网络系统应用总线技术对分布于列车上的设备进行控制,属于一种专用的混合分布式实时系统。随着我国铁路客运进入高速时代,列车通信网络系统的自主研发、设备制造、维护运营等问题成为近年的研究热点。近来,列车通信网络系统研究不断深入,在取得许多成果的同时,有些问题在系统设计过程中变得日益突出,如列车通信网络系统的形式化描述问题、符合列车通信网络标准的行为一致性验证问题等。本文以解决这些问题为目标,以面向应用为出发点,对列车通信网络系统的形式化建模、静态属性分析、动态属性验证和模拟验证等关键技术进行了研究。
本文首先对基于形式化方法和模拟方法的列车系统建模及验证的相关研究进行了综述,以列车系统的设计和验证流程为主线,从列车通信网络标准的分类、列车通信网络系统的形式化建模、动态属性验证、模拟验证等方面进行了研究,总结了该领域存在的问题和下一步的研究方向。
综合运用形式化语义、数学理论分析、模型检查和模拟验证技术,提出了一种适用于列车通信网络系统的形式化建模和验证方法,为列车通信网络系统的设计和验证提供了系统级的解决方案。
深入分析了IEC61375列车通信网络协议,将列车通信网络建模划分为网络拓扑结构和网络功能节点建模两部分工作,提出了一种分层次的列车通信网络系统形式化建模方法,为了满足建模需求,对Petri网进行扩展得到层次实时有色Petri网,建立了完整的列车通信网络系统模型,验证了形式化建模方法的有效性。
以列车通信网络标准和系统特征为依据,定义了列车通信网络系统的HRTCPN模型的静态属性,并以线性代数、图论等数学方法为基础提出了静态属性的检测规则。此外,基于关联矩阵和S-不变量运算对系统模型的实时性分析进行了研究,提出了一种系统时间参数的评估方法和系统实时性能优化方案。
针对已有方法在列车通信系统动态属性验证方面存在的完整性问题,提出了一种系统模型的形式化验证方法,以时间自动机模型和符号模型检查理论为基础,设计了HRTCPN模型到形式化验证输入语义的转换规则,并且基于假设／保证组合检查策略提出了系统的分解方法和假设、保证规则、完整地提取了动态属性,有效避免了状态空间爆炸问题,提高了针对列车通信网络标准进行动态属性验证的完整性。
列车通信网络系统协议大部分主要功能都在网络控制器中实现,对网络控制器的验证在某种意义上等同于系统协议实现级别的验证。基于高级验证方法学构造了列车通信网络控制器的模块级和系统级功能验证模型,设计了网络拓扑级验证模型,弥补了传统验证方法难以模拟通信过程的不足。提出了基于功能覆盖率的驱动测试生成方法、对多重覆盖率收集技术和组件重用技术进行了研究,优化了验证环境。根据列车通信网络标准和一致性测试标准设计了错误注入方法,解决了异常处理机制的验证问题,显著提高了验证的覆盖率和缺陷识别率。
最后,总结论文工作,并提出了下一步的研究方向。
With the technical development of fieldbus, computer network communication, embedded system and fault diagnosis, the modern train control system has been developed from digital control system to distributed computer system which is based on network control system. Train network control system which is a special real-time distributed control system can interconnect and control all of the equipments with bus technology. As the coming of high-speed times of railway, self design and research, equipment manufacture, operation and maintenance of train communication network (TCN) system has become the focus of research. Recently, with the thoroughly study of TCN system, some important achievement has been acquired, but some problems such as formal modeling of TCN system and verification of consistency according to TCN standards are becoming more and more obvious in the development of TCN system. This dissertation aims to propose application-oriented new schemes to solve the problems.
The achievements about modeling and verification of railway system based on formal and simulation methods are surveyed first. The main line to development flow of TCN system, the classification of TCN standards and the technologies about formal modeling, formal verification and simulation are studied. Some problems in this field are concluded.
A rounded framework for formal modeling and verification of TCN system is proposed, which can satisfy the design and verification requirements of TCN system based on technologies of formal sematic, mathematical theory, model checking and simulation.
According to the characteristics of TCN system, a hierachical methodology for modeling is described based on the extended Petri net. As validation of the methodology, HRTCPN is used in extracting behaviors and properties of system, and network topology and nodes functional model of TCN system are constructed.
Definitions of static properties of HRTCPN model about TCN system is described based on TCN standards and characteristics of the system. After that, the checking rules about static properties are illustrated based on mathematical theories such as linear algebra, graph theory, and etc. Moreover, real-time property of TCN system model is studied based on incidence matrix and S-invariables, and real-time analysis methods and optimization methods are proposed.
With the purpose of verification about the dynamic properties of TCN system model, formal verification methodologies based on symbolic model checking and timed automation are given. The transformational rules to the two models from HRTCPN are designed by studying the concepts of symbolic model checing and semantic of timed automation. Dynamic properties of TCN system are verified by means of the combination of the two methodologies, which avoid the states explosion problem owning to hierarchical feature of modeling and verification flow. At the same time, the completeness of dynamic properties verification according to IEC61375 standards is improved.
Most of the major functions about TCN protocol is implemented by TCN controller, and it's very important for the verification of TCN controller in the implementation level. Based on the advanced verification methodology, VMM verification methodology, module level and system-level functional verification frameworks are constructed, and network topology level functional verification framework is proposed aiming to covering the shortage of inefficiency of traditional methods about simulation of communications in the network. Mechanisms such as coverage-driven stimuli generation, multi-level coverage collection and sub-unit reuse are adopted for improving the efficiency of simulation. Error injection mechanism is designed on the basis of requirement of reliability in TCN standards which is a solution to the problem of verification about abnormal processing module in TCN controllers. Furthermore, TCN controllers are verified by employing a full range of methods. As a result, the coverage rate and number of bugs identified are greatly improved.
Finally, the work of the dissertation is concluded.
本文首先对基于形式化方法和模拟方法的列车系统建模及验证的相关研究进行了综述,以列车系统的设计和验证流程为主线,从列车通信网络标准的分类、列车通信网络系统的形式化建模、动态属性验证、模拟验证等方面进行了研究,总结了该领域存在的问题和下一步的研究方向。
综合运用形式化语义、数学理论分析、模型检查和模拟验证技术,提出了一种适用于列车通信网络系统的形式化建模和验证方法,为列车通信网络系统的设计和验证提供了系统级的解决方案。
深入分析了IEC61375列车通信网络协议,将列车通信网络建模划分为网络拓扑结构和网络功能节点建模两部分工作,提出了一种分层次的列车通信网络系统形式化建模方法,为了满足建模需求,对Petri网进行扩展得到层次实时有色Petri网,建立了完整的列车通信网络系统模型,验证了形式化建模方法的有效性。
以列车通信网络标准和系统特征为依据,定义了列车通信网络系统的HRTCPN模型的静态属性,并以线性代数、图论等数学方法为基础提出了静态属性的检测规则。此外,基于关联矩阵和S-不变量运算对系统模型的实时性分析进行了研究,提出了一种系统时间参数的评估方法和系统实时性能优化方案。
针对已有方法在列车通信系统动态属性验证方面存在的完整性问题,提出了一种系统模型的形式化验证方法,以时间自动机模型和符号模型检查理论为基础,设计了HRTCPN模型到形式化验证输入语义的转换规则,并且基于假设／保证组合检查策略提出了系统的分解方法和假设、保证规则、完整地提取了动态属性,有效避免了状态空间爆炸问题,提高了针对列车通信网络标准进行动态属性验证的完整性。
列车通信网络系统协议大部分主要功能都在网络控制器中实现,对网络控制器的验证在某种意义上等同于系统协议实现级别的验证。基于高级验证方法学构造了列车通信网络控制器的模块级和系统级功能验证模型,设计了网络拓扑级验证模型,弥补了传统验证方法难以模拟通信过程的不足。提出了基于功能覆盖率的驱动测试生成方法、对多重覆盖率收集技术和组件重用技术进行了研究,优化了验证环境。根据列车通信网络标准和一致性测试标准设计了错误注入方法,解决了异常处理机制的验证问题,显著提高了验证的覆盖率和缺陷识别率。
最后,总结论文工作,并提出了下一步的研究方向。
With the technical development of fieldbus, computer network communication, embedded system and fault diagnosis, the modern train control system has been developed from digital control system to distributed computer system which is based on network control system. Train network control system which is a special real-time distributed control system can interconnect and control all of the equipments with bus technology. As the coming of high-speed times of railway, self design and research, equipment manufacture, operation and maintenance of train communication network (TCN) system has become the focus of research. Recently, with the thoroughly study of TCN system, some important achievement has been acquired, but some problems such as formal modeling of TCN system and verification of consistency according to TCN standards are becoming more and more obvious in the development of TCN system. This dissertation aims to propose application-oriented new schemes to solve the problems.
The achievements about modeling and verification of railway system based on formal and simulation methods are surveyed first. The main line to development flow of TCN system, the classification of TCN standards and the technologies about formal modeling, formal verification and simulation are studied. Some problems in this field are concluded.
A rounded framework for formal modeling and verification of TCN system is proposed, which can satisfy the design and verification requirements of TCN system based on technologies of formal sematic, mathematical theory, model checking and simulation.
According to the characteristics of TCN system, a hierachical methodology for modeling is described based on the extended Petri net. As validation of the methodology, HRTCPN is used in extracting behaviors and properties of system, and network topology and nodes functional model of TCN system are constructed.
Definitions of static properties of HRTCPN model about TCN system is described based on TCN standards and characteristics of the system. After that, the checking rules about static properties are illustrated based on mathematical theories such as linear algebra, graph theory, and etc. Moreover, real-time property of TCN system model is studied based on incidence matrix and S-invariables, and real-time analysis methods and optimization methods are proposed.
With the purpose of verification about the dynamic properties of TCN system model, formal verification methodologies based on symbolic model checking and timed automation are given. The transformational rules to the two models from HRTCPN are designed by studying the concepts of symbolic model checing and semantic of timed automation. Dynamic properties of TCN system are verified by means of the combination of the two methodologies, which avoid the states explosion problem owning to hierarchical feature of modeling and verification flow. At the same time, the completeness of dynamic properties verification according to IEC61375 standards is improved.
Most of the major functions about TCN protocol is implemented by TCN controller, and it's very important for the verification of TCN controller in the implementation level. Based on the advanced verification methodology, VMM verification methodology, module level and system-level functional verification frameworks are constructed, and network topology level functional verification framework is proposed aiming to covering the shortage of inefficiency of traditional methods about simulation of communications in the network. Mechanisms such as coverage-driven stimuli generation, multi-level coverage collection and sub-unit reuse are adopted for improving the efficiency of simulation. Error injection mechanism is designed on the basis of requirement of reliability in TCN standards which is a solution to the problem of verification about abnormal processing module in TCN controllers. Furthermore, TCN controllers are verified by employing a full range of methods. As a result, the coverage rate and number of bugs identified are greatly improved.
Finally, the work of the dissertation is concluded.
引文
[1]王苏敬.列车用CAN总线应用层协议研究与实现.北京交通大学学报(自然科学版),2008,32(5)95-104页
[2]杨志仁,王雪梅,倪文波.基于Lon Works技术的列车通信网络.测控技术,2000,(06)：13-30页
[3]赵红卫,郑雪洋,王欣,等WorldFIP通讯网络技术的研究与开发.铁道机车车辆,2003,23(S2)：60-64页
[4]左峰,王立德,聂晓波,等.基于ARCNET的轻轨列车通信网络.电力机车与城轨车辆,2009,32(6)27-29页
[5]严云升.列车通信网络(TCN)配置及传送数据的规范化.电力机车技术,2002,25(02)：1-4页
[6]常振臣,牛得田,王立德,等.基于TCN标准的智能显示单元在动车组上的应用研究.电力机车与城轨车辆,2006,29(2)：7-10页
[7]袁嫒.CAN总线在机车微机控制系统中的应用研究.大连交通大学硕士学位论文.2007：20-54页
[8]马云双LONWORKS网络控制技术在内燃动车组控制系统中的应用研究.北京交通大学硕士学位论文.2001：32-69页
[9]杨子亮.列车控制网络的实时性与可靠性研究.西南交通大学硕士学位论文.2008：15-36页
[10]刘洋.基于TCN标准的电动车组网络控制实验平台的设计与实现.大连交通大学硕士学位论文.2009：36-51页
[11]Delatour J, Paludetto M. UML/PNO:A way to merge UML and Petri Net Objects for the analysis of Real-Time Systems. Object-Oriented Technology,1998,1543:511-514P
[12]Aghasaryan A, Fabre E, Benveniste A, et al. Fault detection and diagnosis in distributed systems:An approach by partially stochastic Petri nets. Discrete Event Dynamic Systems-Theory and Applications,1998,8(2):203-231P
[13]Siveroni I, Zisman A, Spanoudakis G. A UML-based static verification framework for security. Requirements Engineering,2010,15(1):95-118P
[14]Niewiadomski A, Penczek W, Szreter M. A New Approach to Model Checking of UML State Machines. Fundamenta Informaticae,2009,93(1-3):289-303P
[15]McLaughlin MJ, Moore A. Real-time extensions to UML. Dr Dobbs Journal, 1998,23(12):82-83P
[16]陈江,陈建国,陆慧娟,等.UML时间顺序图的实时系统建模及验证.中国计量学院学报,2010,21(01)：46-51页
[17]王成军,王星星.UML活动图到Petri网映射方法的研究与实现.微计算机信息,2009,25(2-3)：258-260页
[18]吴志芳,刘听.UML图表到SVG图形转换方法研究.华中电力,2009,22(01)：1-6页
[19]Aredo DB. A framework for semantics of UML sequence diagrams in PVS. Journal of Universal Computer Science,2002,8(7):674-697P
[20]Ober I, Graf S, Ober I. Validation of UML models via a mapping to communicating extended timed automata. Model Checking Software,2004,2989:127-145P
[21]陈为雄,张闯,黄根生.基于UMLTCN网络分析.铁道机车车辆,2009,29(03)：15-19页
[22]王宏刚,张一军,张琦,等.基于UML的列车运行调度系统软件模型.中国铁道科学,2005,26(05)：107-111页
[23]王婷,唐涛.基于UML的城市轨道交通列车控制系统分析与建模.系统仿真学报,2005,17(08)：1993-1996页
[24]黄友能,唐涛.基于UML的城轨列车运行控制仿真系统建模与实现.北京交通大学学报,2007,31(05)：31-34页
[25]白雪,肖宝弟,刘皓玮.基于场景设计的列车调度系统需求建模方法.中国铁道科学,2009,30(03)：115-118页
[26]胡红革,谢阅,黄大贵.基于位置不变量的Petri网分解方法.电子测量与仪器学报,2004,18(02)：77-80页
[27]Bergenthum R, Mauser S, Lorenz R, et al. Unfolding Semantics of Petri Nets Based on Token Flows. Fundamenta Informaticae,2009,94(3-4):331-360P
[28]王安荣.Petri网基本信标的求取算法及死锁避免策略研究.西安电子科技大学博士学位论文.2009：18-39页
[29]叶剑虹.Petri网若干关键技术的研究及其应用.电子科技大学博士学位论文.2009：43-68页
[30]徐雅斌,郭庆凯,罗四维.铁路信号逻辑的计算机辅助分析与设计.北方交通大学学报,1988,(02)：37-42页
[31]张恒巍,杜彦华,汤光明,等.基于多线程的列车群Petri网运行模型的实现.计算机应用,2002,22(10)：76-78页
[32]龙志强,张永焘,叶俊.基于Petri Fault Net的磁浮列车悬浮系统故障分析.系统仿真学报,2007,19(S1)：266-270页
[33]Garrido JL, Gea M. A Coloured Petri Net formalisation for a UML-based notation applied to cooperative system modelling. Interactive Systems:Design, Specification and Verification,2002,2545:16-28P
[34]胡晓辉,党建武,周兴社.针对面向对象着色Petri网的中国列车运行控制系统建模.甘肃科学学报,2005,17(03)：99-103页
[35]吴东勇,张勇.基于通信的列车控制系统的有色Petri网模型的研究.系统仿真学报,2005,17(10)：81-84页
[36]徐田华,唐涛.基于有色Petri网的ETCS通信系统与列车间隔分析.系统仿真学报,2007,19(21)：5038-5041页
[37]吴维敏,董利达,苏宏业,等.基于抑制弧Petri网的离散事件系统的监控理论综述.浙江大学学报(工学版),2003,37(01)：44-48页
[38]乔爽,顾宏,王伟.基于抑制弧Petri网的移动商务过程建模及重构.管理工程学报,2009,(01)：88-92页
[39]傅游,花嵘,田银花.基于带抑制弧的Petri网的min-min算法模型研究.计算机应用研究,2010,(01)：79-82页
[40]何建伟,姚淑珍.基于Petri网的状态机变迁的形式化方法研究.系统仿真学报,2007,19(S1)：65-68页
[41]孟宪福,张晓燕.基于排队理论的对等网络任务调度模型.计算机集成制造系统,2009,15(11)：2140-2146页
[42]蒋昌俊.功能确定的离散并发系统的Petri网规范设计方法.计算机学报,1995,18(07)：532-538页
[43]蒋昌俊,郑应平,疏松桂.非确定并发系统设计的Petri网形式化方法.系统仿真学报,1996,8(04)：37-46页
[44]李海波,战德臣,徐晓飞.工作流业务规则语义的完整性验证技术.计算机研究与发展,2009,46(07)：1143-1151页
[45]吴哲辉,王培良.逻辑电路的增广PETRI网模拟和分析.山东矿业学院学报,1985,11(02)：16-23页
[46]丁志军,蒋昌俊.并发程序验证的时序Petri网方法.计算机学报,2002,25(05)： 467-475页
[47]杜军威,徐中伟.基于时序Petri网的联锁逻辑形式建模与验证.计算机工程与应用,2007,43(13)：7-10页
[48]Merlin P. A Study of the Recoverability of Computing Systems[dissertation]. Irvine: Univ. California,1974
[49]Ramchandani C. Analysis of Asynchronous Concurrent Systems by Timed Petri Nets[dissertation]. Cambridge, Massachusetts,1974
[50]张稳.模糊Petri网在实时系统中的应用研究.华东师范大学硕士学位论文.2006：15-32页
[51]陈艾.面向能耗优化的分布式实时系统调度算法研究.中国科学技术大学博士学位论文.2007：32-49页
[52]王海峰,刘顺利,操红武.基于模糊Petri网的实时系统功能模型构建.现代防御技术.2005,33(3)：61-68页
[53]吴琼,邵志清,刘刚,等.基于着色时间Petri网的实时系统的形式验证.计算机科学.2008,35(7)：257-260页
[54]I. Kamwa, B. Saulnier and R. Reid. Petri Net Based Specification of a Real-Time Supervisory Controller for an Autonomous Wind Diesel System. Electric Power Systems Research.1991,21 (3):203-216P
[55]YK. Lee, SJ. Park. Opnets-an Object-Oriented High-Level Petri Net Model for Real-Time System Modeling. Journal of Systems and Software.1993,20(1):69-86P
[56]D. Gurovic, W. Fengler and J. Nutzel. Development of real-time system specifications through the refinement of duration interval Petri nets. Smc 2000 Conference Proceedings:2000 Ieee International Conference on Systems, Man & Cybernetics. 2000,1:3092-3103P
[57]M. Uzam, A. H. Jones and I. Yucel. Using a Petri-net-based approach for the real-time supervisory control of an experimental manufacturing system. International Journal of Advanced Manufacturing Technology.2000,16(7):498-515P
[58]Alur R, Dill D. The Theory of Timed Automata. Lecture Notes in Computer Science, 1992,600:45-73P
[59]陈伟,薛云志,赵琛,等.一种基于时间自动机的实时系统测试方法.软件学报,2007,18(01)：62-73页
[60]Hune T, Romijn J, Stoelinga M, et al. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming,2002,52-3:183-220P
[61]郭华,庄雷,张习勇UPPAAL-——一种适合自动验证实时系统的工具.微计算机信息,2006,22(15)：52-54页
[62]姬莉霞,李俊锋,张雷.实时系统验证工具UPPAAL光盘技术,2006,(01)：47-49页
[63]Tripakis S. Checking Timed Buchi Automata Emptiness on Simulation Graphs. Acm Transactions on Computational Logic,2009,10(3):20-25P
[64]高冠龙,周清雷.时间自动机与网络协议验证.计算机工程,2006,(22)：130-132页
[65]Yamane S. Formal specification and verification method of concurrent and distributed systems by restricted timed automata. Transformation-Based Reactive Systems Development,1997,1231:169-183P
[66]周清雷,姬莉霞.基于时间自动机的道岔自动控制研究.控制工程,2004,11(S1)：146-149页
[67]陈冰,周祖德,陈幼平,等.基于时间自动机的CAN网络可调度性分析.计算机工程与科学,2006,28(09)：25-27页
[68]刘瑞成,张立臣.基于面向方面的实时系统建模方法.计算机科学,2006,33(07)：262-265页
[69]吕继东,唐涛,燕飞,等.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证.铁道学报,2009,31(03)：59-64页
[70]魏臻,陆阳,汤俊,等.基于自动机模型的平面调车软件设计方法.电子学报,2009,37(05)：1013-1018页
[71]Brock B, Kaufmann M, Moore JS. ACL2 theorems about commercial microprocessors. Formal Methods in Computer-Aided Design,1996,1166:275-293P
[72]Hunt WA, Kaufmann M, Krug RB, et al. Meta reasoning in ACL2. Theorem Proving in Higher Order Logics, Proceedings,2005,3603:163-178P
[73]Medina-Bulo I, Palomo-Lozano F, Ruiz-Reina JL. A verified COMMON LISP implementation of Buchberger's algorithm in ACL2. Journal of Symbolic Computation, 2010,45(1):96-123P
[74]Ruess H. Hierarchical verification of two-dimensional high-speed multi-plication in PVS:A case study. Formal Methods in Computer-Aided Design,1996,1166:79-93P
[75]Canovas-Dumas C, Caspi P. A PVS proof obligation generator for Lustre programs. Logic for Programming and Automated Reasoning, Proceedings,2000,1955:179-188P
[76]Evans N, Schneider S. Analysing time dependent security properties in CSP using PVS. Computer Security-Esorics 2000, Proceedings,2000,1895:222-237P
[77]Umeno S, Lynch N. Proving safety properties of an aircraft landing protocol using I/O automata and the PVS theorem prover:A case study. Fm 2006:Formal Methods, Proceedings,2006,4085:64-80P
[78]Vaandrager FW, de Groot AL. Analysis of a biphase mark protocol with UPPAAL and PVS. Formal Aspects of Computing,2006,18(4):433-458P
[79]Agerholm S. Lcf Examples in Hol. Computer Journal,1995,38(2):121-130P
[80]Windley PJ. Abstract Theories in Hol. Ifip Transactions a-Computer Science and Technology,1993,20:197-21 OP
[81]Alvesfoss J. Modeling Nondeterministic Systems in Hol. Ifip Transactions a-Computer Science and Technology,1993,20:295-304P
[82]Angelo CM, Claesen L, Deman H. Modeling Multirate Dsp Specification Semantics for Formal Transformational Design in Hol. Formal Methods in System Design, 1994,5(1-2):61-94P
[83]Reetz R, Kropf T. A Flowgraph Semantics of Vhdl-toward a Vhdl Verification Workbench in Hol. Formal Methods in System Design,1995,7(1-2):73-99P
[84]Choi BD, Lee Y, Choi DL. Geo(xl), Geo(x2)/D/c HOL priority queueing system with random order selection within each priority class. Probability in the Engineering and Informational Sciences,1998,12(1):125-139P
[85]Clarke EM, Kurshan RP. Computer-aided verification. IEEE Spectrum,1996,33(6): 61-67P
[86]Clarke E, Emerson E. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Proceedings of the Workshop on Logic of Programs, LNCS, Springer-Verlag,1981,131:52-71P
[87]Queille P, Sifakia J. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming, LNCS, Springer-Verlag,1982,137: 337-351P
[88]Rajkumar PV, Ghosh SK, Dasgupta P. Concurrent Usage Control Implementation Verification Using the SPIN Model Checker. Recent Trends in Network Security and Applications,2010,89,214-223P
[89]Melatti I, Palmer R, Sawaya G, Yang Y. Distributed Dynamic Partial Order Reduction. International Journal on Software Tools for Technology Transfer (STTT).2010,12(2): 113-122P
[90]Jaghoori MM, Sirjani M, Mousavi MR. Symmetry and partial order reduction techniques in model checking Rebeca. Acta Informatica.2010,47(1):33-66P
[91]Akers SB. Binary Decision Diagrams. In IEEE Transactions on Computers,1978,6: 509-516P
[92]Bryant RE. Graph-Based Algorithms for Boolean Function Manipulation. In IEEE Transactions on Computers,1986,8:677-691P
[93]Clarke EM. The Birth of Model Checking.25 Years of Model Checking. Lecture Notes in Computer Science,2008,5000:1-26P
[94]Alessandro F, Maurizio M, Margherita N. A NuSMV Extension for Graded-CTL Model Checking. Computer Aided Verification. Lecture Notes in Computer Science,2010, V6174:670-673P,
[95]Sehun J, Junbeom Y, Sungdeok C. VIS Analyzer:A Visual Assistant for VIS Verification and Analysis. IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC), Carmona Seville,2010:250-254P
[96]Shoham BD, Richard T, Grant W. Model Checking Using Description Logic. Journal of Logic and Computation.2010,20(1):111-131P
[97]Biere A, Cimatti A, Clarke E. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction, LNCS, 1999,1579:193-207P
[98]McMillan KL. Symbolic Model Checking:An Approach to the State Explosion Problem[dissertation]. Kluwer Academic,1993
[99]Mohamed OA, Song XY, Cerny E, et al. MDG-based state enumeration by retiming and circuit transformation. Journal of Circuits Systems and Computers,2004,13(5): 1111-1132P
[100]Bhadra J, Krishnamurthy N, Abadir MS. Enhanced equivalence checking-Toward a solidarity of functional verification and manufacturing test generation. IEEE Design & Test of Computers,2004,21(6):494-502P
[101]Mathur A, Clarke E, Fujita M, et al. Functional Equivalence Verification Tools in High-Level Synthesis Flows. IEEE Design & Test of Computers,2009,26(4):88-95P
[102]Gawanmeh A, Tahar S, Winter K. Interfacing ASM with the MDG tool. Abstract State Machines 2003:Advances in Theory and Practic, Proceedings,2003,2589:278-292P
[103]高秋红.时序电路的功能验证方法和技术研究.北京交通大学硕士学位论文.2006：40-66页
[104]陈华宏.64位高性能微处器系统功能验证方法的研究与实现.国防科学技术大学硕士学位论文.2005：45-72页
[105]Cupak M, Catthoor F, De Man HJ. Efficient system-level functional verification methodology for multimedia applications. IEEE Design & Test of Computers, 2003,20(2):56-64P
[106]Brauer EJ, Kang SM. An Algorithm for Functional Verification of Digital Eel Circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1995,14(12):1546-1556P
[107]董玲.IP核设计中功能验证的研究与应用.江南大学硕士学位论文,2006：36-61页
[108]Da Silva KRG, Melcher EUK, Maia I, et al. A methodology aimed at better integration of functional verification and RTL design. Design Automation for Embedded Systems, 2005,10(4):285-298P
[109]Anon. Cycle-based simulator addresses functional verification challenge. Electronic Design,1997,45(20):88-90P
[110]Bruschi F, Ferrandi F, Sciuto D. A framework for the functional verification of SystemC models. International Journal of Parallel Programming,2005,33(6):667-695P
[111]Drobushevich GA, Zubovich KA. Automatic Verification of Functional Programs. Cybernetics,1990,26(4):491-502P
[112]孙立宏,洪一.基于VMM统一验证平台的处理器芯片功能验证.火控雷达技术,2010,39(01)：45-48页
[113]Guzey O, Wang LC, Levitt JR, et al. Increasing the Efficiency of Simulation-Based Functional Verification Through Unsupervised Support Vector Analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2010,29(1):138-148P
[114]Kakoee MR, Neishaburi MH, Mohammadi S. Graph based test case generation for TLM functional verification. Microprocessors and Microsystems,2008,32(5-6): 288-295P
[115]Chockler H, Kupferman O, Vardi MY. Coverage metrics for formal verification. Correct Hardware Design and Verification Methods, Proceedings,2003,2860: 111-125P
[116]王赵君.北桥芯片功能验证中的覆盖率分析.中国科学院研究生院硕士学位论文.2005：35-52页
[117]Fallah F, Devadas S, Keutzer K. OCCOM-Efficient computation of observability-based code coverage metrics for functional verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2001,20(8):1003-1015P
[118]罗春.基于仿真的系统芯片功能验证技术研究.东南大学博士学位论文.2006：51-89页
[119]鲁巍.模拟验证中的激励产生与覆盖评估.中国科学院研究生院博士学位论文,2006：68-93页
[120]Lv T, Fan JP, Li XW, et al. Observability statement coverage based on dynamic factored use-definition chains for functional verification. Journal of Electronic Testing-Theory and Applications,2006,22(3):273-285P
[121]Madl G, Pasricha S, Dutt N, et al. Cross-Abstraction Functional Verification and Performance Analysis of Chip Multiprocessor Designs. IEEE Transactions on Industrial Informatics,2009,5(3):241-256P
[122]Abdurazik A, Offutt J. Using UML collaboration diagrams for static checking and test generation. Uml 2000-the Unified Modeling Language, Proceedings,2000,1939: 383-395P
[123]席筱颖.8位MCU设计验证及测试向量故障覆盖率分析.哈尔滨理工大学硕士学位论文.2007：23-46页
[124]Bhadra J, Abadir MS, Ray S, et al. A survey of hybrid techniques for functional verification. IEEE Design & Test of Computers,2007,24(2):112-122P
[125]Aura T, Lilius J. A causal semantics for time Petri nets. Theoretical Computer Science, 2000,243(1-2):409-447P
[126]Meyer M, Schnieder E. Formal modeling and simulation of train control systems using petri nets. Formal Methods,1999,2:1867-1872P
[127]Kluge O. Modelling a Railway Crossing with Message Sequence Charts and Petri Nets. Petri Net Technology for Communication-Based Systems,2003,197-218P
[128]Zimmermann A and Hommel G. Towards modeling and evaluation of ETCS real-time communication and operation. Journal of Systems and Software,2005,1:47-54P
[129]Zimmermann A and Hommel G. Using UML state machines and petri nets for the quantitative investigation of ETCS. Proceedings of the 1st international conference on Performance evaluation methodolgies and tools,2006,504-409P
[130]Barger P, Schon W, Bouali M. A study of railway ERTMS safety with Colored Petri Nets. The European Safety and Reliability Conference,2009,102-108P
[131]吴哲辉编著.Petri网导论.北京：机械工业出版社,2006：14-18页,27-41页,73-96页,285-297页
[132]Peleska J, Grobe D, Haxthausen AE. Automated verification for train control systems. Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems, Braunschweig,2004,113-127P
[133]Climatti A, Roveri M, Tonetta S. Requirements validation for hybrid systems. Computer Aided Verification,2009,5643:188-203P
[134]Swen J, Viorica SS. Applications of hierarchical reasoning in verification of complex systems. Electronic Notes in Theoretical Computer Science,2007,174(8):39-54P
[135]Banci M, Fantechi A, Gnesi S. The Role of Formal Methods in Develping a Distributed Railway Interlocking System. Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems, Braunschweig,2004,221-224P
[136]Armin Z, Gunter H. A Train Control System Case Study in Model-Based Real Time System Design. International Parallel and Distributed Processing Symposium, France, 2003,118-121P
[137]Misra J, Chandy K. Proofs of Networks of Processes. IEEE Transactions on Software Engineering,1981,7(4):417-426P
[138]文艳军,王戟,齐治昌.并发反应式系统的组合模型检验与组合精化检验.软件学报,2007,18(6)：1270-1281P
[139]Kumar JA, Vasudevan S. Automatic compositional reasoning for probabilistic model checking of hardware designs.2010 Seventh International Conference on the Quantitative Evaluation of Systems,2010:143-152P
[140]Moreno JC, Laloya E, Navarro J. A link-layer slave device design of the MVB-TCN bus (IEC 61375 and IEEE 1473-T). IEEE Transactions on Vehicular Techology,2007, 56(6):3457-3468P
[141]Yongxiang W, Lide W, Wenqing L. Design and Implementation of MVB Controller using SOPC Technology. Industrial Electronics and Applications,2007,2666-2669P
[142]Jaime J, Jose L, Martin J. Design of a Master Device for the Multifunction Vehicle Bus. IEEE Transactions on Vehicular Techology,2007 56(6):3695-3708P
[143]杨兵.多功能车辆总线控制器(MVBC)的研究与FPGA设计.电子科技大学硕士学位论文.2006：72-74页
[144]姜娜.WTB底层协议的研究与实现.北京交通大学硕士学位论文.2007：41-46页
[145]计辉.WTB列车总线网的研究与实现.西北工业大学硕士学位论文.2006：54-55页
[146]李庆锋.新一代机车总线控制器(MVBC)的研究与设计.电子科技大学硕士学位论文.2005：71-77页
[147]余金山.模型驱动的SoC系统级功能验证关键技术研究.国防科学技术大学博士学位论文.2007：73-94页
[148]Gharehbaghi AM, Yaran BH, Hessabi S, et al. An assertion-based verification methodology for system-level design. Computers & Electrical Engineering,2007,33(4): 269-284P
[149]Akbarpour B, Abdel-Hamid AT, Tahar S, et al. Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. Computer Journal, 2010,53(4):465-488P
[150]鲁巍.模拟验证中激励产生与覆盖评估.中国科学院研究生院博士学位论文.2006：83-103页
[151]沈海华,卫文丽,陈云霁.覆盖率驱动的随机测试生成技术综述.计算机辅助设计与图形学学报,2009,21(4)：419-431页
[152]丁谢THUASDSP2004处理器功能验证的设计及实现.电子科技大学硕士学位论文.2006：41-67页
[153]Prasad Joshi, Peter A. Beerel, Marly Roncken and Ivan Sutherland. Timing Verification of GasP Asynchronous Circuits:Predicted Delay Variations Observed by Experiment. Concurrency, Compositionality, and Correctness,2010,5930:260-276P
[154]Furumiya T, Ng DC, Yasuoka K, et al. Functional verification of pulse frequency modulation-based image sensor for retinal prosthesis by in vitro electrophysiological experiments using frog retina. Biosensors & Bioelectronics,2006,21(7):1059-1068P
[155]许庆国,缪淮扣.在原型验证系统中构建度量区间时序逻辑公式的时间自动机(英文)Journal of Shanghai University(English Edition),2008,12(04):339-346页
[2]杨志仁,王雪梅,倪文波.基于Lon Works技术的列车通信网络.测控技术,2000,(06)：13-30页
[3]赵红卫,郑雪洋,王欣,等WorldFIP通讯网络技术的研究与开发.铁道机车车辆,2003,23(S2)：60-64页
[4]左峰,王立德,聂晓波,等.基于ARCNET的轻轨列车通信网络.电力机车与城轨车辆,2009,32(6)27-29页
[5]严云升.列车通信网络(TCN)配置及传送数据的规范化.电力机车技术,2002,25(02)：1-4页
[6]常振臣,牛得田,王立德,等.基于TCN标准的智能显示单元在动车组上的应用研究.电力机车与城轨车辆,2006,29(2)：7-10页
[7]袁嫒.CAN总线在机车微机控制系统中的应用研究.大连交通大学硕士学位论文.2007：20-54页
[8]马云双LONWORKS网络控制技术在内燃动车组控制系统中的应用研究.北京交通大学硕士学位论文.2001：32-69页
[9]杨子亮.列车控制网络的实时性与可靠性研究.西南交通大学硕士学位论文.2008：15-36页
[10]刘洋.基于TCN标准的电动车组网络控制实验平台的设计与实现.大连交通大学硕士学位论文.2009：36-51页
[11]Delatour J, Paludetto M. UML/PNO:A way to merge UML and Petri Net Objects for the analysis of Real-Time Systems. Object-Oriented Technology,1998,1543:511-514P
[12]Aghasaryan A, Fabre E, Benveniste A, et al. Fault detection and diagnosis in distributed systems:An approach by partially stochastic Petri nets. Discrete Event Dynamic Systems-Theory and Applications,1998,8(2):203-231P
[13]Siveroni I, Zisman A, Spanoudakis G. A UML-based static verification framework for security. Requirements Engineering,2010,15(1):95-118P
[14]Niewiadomski A, Penczek W, Szreter M. A New Approach to Model Checking of UML State Machines. Fundamenta Informaticae,2009,93(1-3):289-303P
[15]McLaughlin MJ, Moore A. Real-time extensions to UML. Dr Dobbs Journal, 1998,23(12):82-83P
[16]陈江,陈建国,陆慧娟,等.UML时间顺序图的实时系统建模及验证.中国计量学院学报,2010,21(01)：46-51页
[17]王成军,王星星.UML活动图到Petri网映射方法的研究与实现.微计算机信息,2009,25(2-3)：258-260页
[18]吴志芳,刘听.UML图表到SVG图形转换方法研究.华中电力,2009,22(01)：1-6页
[19]Aredo DB. A framework for semantics of UML sequence diagrams in PVS. Journal of Universal Computer Science,2002,8(7):674-697P
[20]Ober I, Graf S, Ober I. Validation of UML models via a mapping to communicating extended timed automata. Model Checking Software,2004,2989:127-145P
[21]陈为雄,张闯,黄根生.基于UMLTCN网络分析.铁道机车车辆,2009,29(03)：15-19页
[22]王宏刚,张一军,张琦,等.基于UML的列车运行调度系统软件模型.中国铁道科学,2005,26(05)：107-111页
[23]王婷,唐涛.基于UML的城市轨道交通列车控制系统分析与建模.系统仿真学报,2005,17(08)：1993-1996页
[24]黄友能,唐涛.基于UML的城轨列车运行控制仿真系统建模与实现.北京交通大学学报,2007,31(05)：31-34页
[25]白雪,肖宝弟,刘皓玮.基于场景设计的列车调度系统需求建模方法.中国铁道科学,2009,30(03)：115-118页
[26]胡红革,谢阅,黄大贵.基于位置不变量的Petri网分解方法.电子测量与仪器学报,2004,18(02)：77-80页
[27]Bergenthum R, Mauser S, Lorenz R, et al. Unfolding Semantics of Petri Nets Based on Token Flows. Fundamenta Informaticae,2009,94(3-4):331-360P
[28]王安荣.Petri网基本信标的求取算法及死锁避免策略研究.西安电子科技大学博士学位论文.2009：18-39页
[29]叶剑虹.Petri网若干关键技术的研究及其应用.电子科技大学博士学位论文.2009：43-68页
[30]徐雅斌,郭庆凯,罗四维.铁路信号逻辑的计算机辅助分析与设计.北方交通大学学报,1988,(02)：37-42页
[31]张恒巍,杜彦华,汤光明,等.基于多线程的列车群Petri网运行模型的实现.计算机应用,2002,22(10)：76-78页
[32]龙志强,张永焘,叶俊.基于Petri Fault Net的磁浮列车悬浮系统故障分析.系统仿真学报,2007,19(S1)：266-270页
[33]Garrido JL, Gea M. A Coloured Petri Net formalisation for a UML-based notation applied to cooperative system modelling. Interactive Systems:Design, Specification and Verification,2002,2545:16-28P
[34]胡晓辉,党建武,周兴社.针对面向对象着色Petri网的中国列车运行控制系统建模.甘肃科学学报,2005,17(03)：99-103页
[35]吴东勇,张勇.基于通信的列车控制系统的有色Petri网模型的研究.系统仿真学报,2005,17(10)：81-84页
[36]徐田华,唐涛.基于有色Petri网的ETCS通信系统与列车间隔分析.系统仿真学报,2007,19(21)：5038-5041页
[37]吴维敏,董利达,苏宏业,等.基于抑制弧Petri网的离散事件系统的监控理论综述.浙江大学学报(工学版),2003,37(01)：44-48页
[38]乔爽,顾宏,王伟.基于抑制弧Petri网的移动商务过程建模及重构.管理工程学报,2009,(01)：88-92页
[39]傅游,花嵘,田银花.基于带抑制弧的Petri网的min-min算法模型研究.计算机应用研究,2010,(01)：79-82页
[40]何建伟,姚淑珍.基于Petri网的状态机变迁的形式化方法研究.系统仿真学报,2007,19(S1)：65-68页
[41]孟宪福,张晓燕.基于排队理论的对等网络任务调度模型.计算机集成制造系统,2009,15(11)：2140-2146页
[42]蒋昌俊.功能确定的离散并发系统的Petri网规范设计方法.计算机学报,1995,18(07)：532-538页
[43]蒋昌俊,郑应平,疏松桂.非确定并发系统设计的Petri网形式化方法.系统仿真学报,1996,8(04)：37-46页
[44]李海波,战德臣,徐晓飞.工作流业务规则语义的完整性验证技术.计算机研究与发展,2009,46(07)：1143-1151页
[45]吴哲辉,王培良.逻辑电路的增广PETRI网模拟和分析.山东矿业学院学报,1985,11(02)：16-23页
[46]丁志军,蒋昌俊.并发程序验证的时序Petri网方法.计算机学报,2002,25(05)： 467-475页
[47]杜军威,徐中伟.基于时序Petri网的联锁逻辑形式建模与验证.计算机工程与应用,2007,43(13)：7-10页
[48]Merlin P. A Study of the Recoverability of Computing Systems[dissertation]. Irvine: Univ. California,1974
[49]Ramchandani C. Analysis of Asynchronous Concurrent Systems by Timed Petri Nets[dissertation]. Cambridge, Massachusetts,1974
[50]张稳.模糊Petri网在实时系统中的应用研究.华东师范大学硕士学位论文.2006：15-32页
[51]陈艾.面向能耗优化的分布式实时系统调度算法研究.中国科学技术大学博士学位论文.2007：32-49页
[52]王海峰,刘顺利,操红武.基于模糊Petri网的实时系统功能模型构建.现代防御技术.2005,33(3)：61-68页
[53]吴琼,邵志清,刘刚,等.基于着色时间Petri网的实时系统的形式验证.计算机科学.2008,35(7)：257-260页
[54]I. Kamwa, B. Saulnier and R. Reid. Petri Net Based Specification of a Real-Time Supervisory Controller for an Autonomous Wind Diesel System. Electric Power Systems Research.1991,21 (3):203-216P
[55]YK. Lee, SJ. Park. Opnets-an Object-Oriented High-Level Petri Net Model for Real-Time System Modeling. Journal of Systems and Software.1993,20(1):69-86P
[56]D. Gurovic, W. Fengler and J. Nutzel. Development of real-time system specifications through the refinement of duration interval Petri nets. Smc 2000 Conference Proceedings:2000 Ieee International Conference on Systems, Man & Cybernetics. 2000,1:3092-3103P
[57]M. Uzam, A. H. Jones and I. Yucel. Using a Petri-net-based approach for the real-time supervisory control of an experimental manufacturing system. International Journal of Advanced Manufacturing Technology.2000,16(7):498-515P
[58]Alur R, Dill D. The Theory of Timed Automata. Lecture Notes in Computer Science, 1992,600:45-73P
[59]陈伟,薛云志,赵琛,等.一种基于时间自动机的实时系统测试方法.软件学报,2007,18(01)：62-73页
[60]Hune T, Romijn J, Stoelinga M, et al. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming,2002,52-3:183-220P
[61]郭华,庄雷,张习勇UPPAAL-——一种适合自动验证实时系统的工具.微计算机信息,2006,22(15)：52-54页
[62]姬莉霞,李俊锋,张雷.实时系统验证工具UPPAAL光盘技术,2006,(01)：47-49页
[63]Tripakis S. Checking Timed Buchi Automata Emptiness on Simulation Graphs. Acm Transactions on Computational Logic,2009,10(3):20-25P
[64]高冠龙,周清雷.时间自动机与网络协议验证.计算机工程,2006,(22)：130-132页
[65]Yamane S. Formal specification and verification method of concurrent and distributed systems by restricted timed automata. Transformation-Based Reactive Systems Development,1997,1231:169-183P
[66]周清雷,姬莉霞.基于时间自动机的道岔自动控制研究.控制工程,2004,11(S1)：146-149页
[67]陈冰,周祖德,陈幼平,等.基于时间自动机的CAN网络可调度性分析.计算机工程与科学,2006,28(09)：25-27页
[68]刘瑞成,张立臣.基于面向方面的实时系统建模方法.计算机科学,2006,33(07)：262-265页
[69]吕继东,唐涛,燕飞,等.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证.铁道学报,2009,31(03)：59-64页
[70]魏臻,陆阳,汤俊,等.基于自动机模型的平面调车软件设计方法.电子学报,2009,37(05)：1013-1018页
[71]Brock B, Kaufmann M, Moore JS. ACL2 theorems about commercial microprocessors. Formal Methods in Computer-Aided Design,1996,1166:275-293P
[72]Hunt WA, Kaufmann M, Krug RB, et al. Meta reasoning in ACL2. Theorem Proving in Higher Order Logics, Proceedings,2005,3603:163-178P
[73]Medina-Bulo I, Palomo-Lozano F, Ruiz-Reina JL. A verified COMMON LISP implementation of Buchberger's algorithm in ACL2. Journal of Symbolic Computation, 2010,45(1):96-123P
[74]Ruess H. Hierarchical verification of two-dimensional high-speed multi-plication in PVS:A case study. Formal Methods in Computer-Aided Design,1996,1166:79-93P
[75]Canovas-Dumas C, Caspi P. A PVS proof obligation generator for Lustre programs. Logic for Programming and Automated Reasoning, Proceedings,2000,1955:179-188P
[76]Evans N, Schneider S. Analysing time dependent security properties in CSP using PVS. Computer Security-Esorics 2000, Proceedings,2000,1895:222-237P
[77]Umeno S, Lynch N. Proving safety properties of an aircraft landing protocol using I/O automata and the PVS theorem prover:A case study. Fm 2006:Formal Methods, Proceedings,2006,4085:64-80P
[78]Vaandrager FW, de Groot AL. Analysis of a biphase mark protocol with UPPAAL and PVS. Formal Aspects of Computing,2006,18(4):433-458P
[79]Agerholm S. Lcf Examples in Hol. Computer Journal,1995,38(2):121-130P
[80]Windley PJ. Abstract Theories in Hol. Ifip Transactions a-Computer Science and Technology,1993,20:197-21 OP
[81]Alvesfoss J. Modeling Nondeterministic Systems in Hol. Ifip Transactions a-Computer Science and Technology,1993,20:295-304P
[82]Angelo CM, Claesen L, Deman H. Modeling Multirate Dsp Specification Semantics for Formal Transformational Design in Hol. Formal Methods in System Design, 1994,5(1-2):61-94P
[83]Reetz R, Kropf T. A Flowgraph Semantics of Vhdl-toward a Vhdl Verification Workbench in Hol. Formal Methods in System Design,1995,7(1-2):73-99P
[84]Choi BD, Lee Y, Choi DL. Geo(xl), Geo(x2)/D/c HOL priority queueing system with random order selection within each priority class. Probability in the Engineering and Informational Sciences,1998,12(1):125-139P
[85]Clarke EM, Kurshan RP. Computer-aided verification. IEEE Spectrum,1996,33(6): 61-67P
[86]Clarke E, Emerson E. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Proceedings of the Workshop on Logic of Programs, LNCS, Springer-Verlag,1981,131:52-71P
[87]Queille P, Sifakia J. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming, LNCS, Springer-Verlag,1982,137: 337-351P
[88]Rajkumar PV, Ghosh SK, Dasgupta P. Concurrent Usage Control Implementation Verification Using the SPIN Model Checker. Recent Trends in Network Security and Applications,2010,89,214-223P
[89]Melatti I, Palmer R, Sawaya G, Yang Y. Distributed Dynamic Partial Order Reduction. International Journal on Software Tools for Technology Transfer (STTT).2010,12(2): 113-122P
[90]Jaghoori MM, Sirjani M, Mousavi MR. Symmetry and partial order reduction techniques in model checking Rebeca. Acta Informatica.2010,47(1):33-66P
[91]Akers SB. Binary Decision Diagrams. In IEEE Transactions on Computers,1978,6: 509-516P
[92]Bryant RE. Graph-Based Algorithms for Boolean Function Manipulation. In IEEE Transactions on Computers,1986,8:677-691P
[93]Clarke EM. The Birth of Model Checking.25 Years of Model Checking. Lecture Notes in Computer Science,2008,5000:1-26P
[94]Alessandro F, Maurizio M, Margherita N. A NuSMV Extension for Graded-CTL Model Checking. Computer Aided Verification. Lecture Notes in Computer Science,2010, V6174:670-673P,
[95]Sehun J, Junbeom Y, Sungdeok C. VIS Analyzer:A Visual Assistant for VIS Verification and Analysis. IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC), Carmona Seville,2010:250-254P
[96]Shoham BD, Richard T, Grant W. Model Checking Using Description Logic. Journal of Logic and Computation.2010,20(1):111-131P
[97]Biere A, Cimatti A, Clarke E. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction, LNCS, 1999,1579:193-207P
[98]McMillan KL. Symbolic Model Checking:An Approach to the State Explosion Problem[dissertation]. Kluwer Academic,1993
[99]Mohamed OA, Song XY, Cerny E, et al. MDG-based state enumeration by retiming and circuit transformation. Journal of Circuits Systems and Computers,2004,13(5): 1111-1132P
[100]Bhadra J, Krishnamurthy N, Abadir MS. Enhanced equivalence checking-Toward a solidarity of functional verification and manufacturing test generation. IEEE Design & Test of Computers,2004,21(6):494-502P
[101]Mathur A, Clarke E, Fujita M, et al. Functional Equivalence Verification Tools in High-Level Synthesis Flows. IEEE Design & Test of Computers,2009,26(4):88-95P
[102]Gawanmeh A, Tahar S, Winter K. Interfacing ASM with the MDG tool. Abstract State Machines 2003:Advances in Theory and Practic, Proceedings,2003,2589:278-292P
[103]高秋红.时序电路的功能验证方法和技术研究.北京交通大学硕士学位论文.2006：40-66页
[104]陈华宏.64位高性能微处器系统功能验证方法的研究与实现.国防科学技术大学硕士学位论文.2005：45-72页
[105]Cupak M, Catthoor F, De Man HJ. Efficient system-level functional verification methodology for multimedia applications. IEEE Design & Test of Computers, 2003,20(2):56-64P
[106]Brauer EJ, Kang SM. An Algorithm for Functional Verification of Digital Eel Circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1995,14(12):1546-1556P
[107]董玲.IP核设计中功能验证的研究与应用.江南大学硕士学位论文,2006：36-61页
[108]Da Silva KRG, Melcher EUK, Maia I, et al. A methodology aimed at better integration of functional verification and RTL design. Design Automation for Embedded Systems, 2005,10(4):285-298P
[109]Anon. Cycle-based simulator addresses functional verification challenge. Electronic Design,1997,45(20):88-90P
[110]Bruschi F, Ferrandi F, Sciuto D. A framework for the functional verification of SystemC models. International Journal of Parallel Programming,2005,33(6):667-695P
[111]Drobushevich GA, Zubovich KA. Automatic Verification of Functional Programs. Cybernetics,1990,26(4):491-502P
[112]孙立宏,洪一.基于VMM统一验证平台的处理器芯片功能验证.火控雷达技术,2010,39(01)：45-48页
[113]Guzey O, Wang LC, Levitt JR, et al. Increasing the Efficiency of Simulation-Based Functional Verification Through Unsupervised Support Vector Analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2010,29(1):138-148P
[114]Kakoee MR, Neishaburi MH, Mohammadi S. Graph based test case generation for TLM functional verification. Microprocessors and Microsystems,2008,32(5-6): 288-295P
[115]Chockler H, Kupferman O, Vardi MY. Coverage metrics for formal verification. Correct Hardware Design and Verification Methods, Proceedings,2003,2860: 111-125P
[116]王赵君.北桥芯片功能验证中的覆盖率分析.中国科学院研究生院硕士学位论文.2005：35-52页
[117]Fallah F, Devadas S, Keutzer K. OCCOM-Efficient computation of observability-based code coverage metrics for functional verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2001,20(8):1003-1015P
[118]罗春.基于仿真的系统芯片功能验证技术研究.东南大学博士学位论文.2006：51-89页
[119]鲁巍.模拟验证中的激励产生与覆盖评估.中国科学院研究生院博士学位论文,2006：68-93页
[120]Lv T, Fan JP, Li XW, et al. Observability statement coverage based on dynamic factored use-definition chains for functional verification. Journal of Electronic Testing-Theory and Applications,2006,22(3):273-285P
[121]Madl G, Pasricha S, Dutt N, et al. Cross-Abstraction Functional Verification and Performance Analysis of Chip Multiprocessor Designs. IEEE Transactions on Industrial Informatics,2009,5(3):241-256P
[122]Abdurazik A, Offutt J. Using UML collaboration diagrams for static checking and test generation. Uml 2000-the Unified Modeling Language, Proceedings,2000,1939: 383-395P
[123]席筱颖.8位MCU设计验证及测试向量故障覆盖率分析.哈尔滨理工大学硕士学位论文.2007：23-46页
[124]Bhadra J, Abadir MS, Ray S, et al. A survey of hybrid techniques for functional verification. IEEE Design & Test of Computers,2007,24(2):112-122P
[125]Aura T, Lilius J. A causal semantics for time Petri nets. Theoretical Computer Science, 2000,243(1-2):409-447P
[126]Meyer M, Schnieder E. Formal modeling and simulation of train control systems using petri nets. Formal Methods,1999,2:1867-1872P
[127]Kluge O. Modelling a Railway Crossing with Message Sequence Charts and Petri Nets. Petri Net Technology for Communication-Based Systems,2003,197-218P
[128]Zimmermann A and Hommel G. Towards modeling and evaluation of ETCS real-time communication and operation. Journal of Systems and Software,2005,1:47-54P
[129]Zimmermann A and Hommel G. Using UML state machines and petri nets for the quantitative investigation of ETCS. Proceedings of the 1st international conference on Performance evaluation methodolgies and tools,2006,504-409P
[130]Barger P, Schon W, Bouali M. A study of railway ERTMS safety with Colored Petri Nets. The European Safety and Reliability Conference,2009,102-108P
[131]吴哲辉编著.Petri网导论.北京：机械工业出版社,2006：14-18页,27-41页,73-96页,285-297页
[132]Peleska J, Grobe D, Haxthausen AE. Automated verification for train control systems. Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems, Braunschweig,2004,113-127P
[133]Climatti A, Roveri M, Tonetta S. Requirements validation for hybrid systems. Computer Aided Verification,2009,5643:188-203P
[134]Swen J, Viorica SS. Applications of hierarchical reasoning in verification of complex systems. Electronic Notes in Theoretical Computer Science,2007,174(8):39-54P
[135]Banci M, Fantechi A, Gnesi S. The Role of Formal Methods in Develping a Distributed Railway Interlocking System. Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems, Braunschweig,2004,221-224P
[136]Armin Z, Gunter H. A Train Control System Case Study in Model-Based Real Time System Design. International Parallel and Distributed Processing Symposium, France, 2003,118-121P
[137]Misra J, Chandy K. Proofs of Networks of Processes. IEEE Transactions on Software Engineering,1981,7(4):417-426P
[138]文艳军,王戟,齐治昌.并发反应式系统的组合模型检验与组合精化检验.软件学报,2007,18(6)：1270-1281P
[139]Kumar JA, Vasudevan S. Automatic compositional reasoning for probabilistic model checking of hardware designs.2010 Seventh International Conference on the Quantitative Evaluation of Systems,2010:143-152P
[140]Moreno JC, Laloya E, Navarro J. A link-layer slave device design of the MVB-TCN bus (IEC 61375 and IEEE 1473-T). IEEE Transactions on Vehicular Techology,2007, 56(6):3457-3468P
[141]Yongxiang W, Lide W, Wenqing L. Design and Implementation of MVB Controller using SOPC Technology. Industrial Electronics and Applications,2007,2666-2669P
[142]Jaime J, Jose L, Martin J. Design of a Master Device for the Multifunction Vehicle Bus. IEEE Transactions on Vehicular Techology,2007 56(6):3695-3708P
[143]杨兵.多功能车辆总线控制器(MVBC)的研究与FPGA设计.电子科技大学硕士学位论文.2006：72-74页
[144]姜娜.WTB底层协议的研究与实现.北京交通大学硕士学位论文.2007：41-46页
[145]计辉.WTB列车总线网的研究与实现.西北工业大学硕士学位论文.2006：54-55页
[146]李庆锋.新一代机车总线控制器(MVBC)的研究与设计.电子科技大学硕士学位论文.2005：71-77页
[147]余金山.模型驱动的SoC系统级功能验证关键技术研究.国防科学技术大学博士学位论文.2007：73-94页
[148]Gharehbaghi AM, Yaran BH, Hessabi S, et al. An assertion-based verification methodology for system-level design. Computers & Electrical Engineering,2007,33(4): 269-284P
[149]Akbarpour B, Abdel-Hamid AT, Tahar S, et al. Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. Computer Journal, 2010,53(4):465-488P
[150]鲁巍.模拟验证中激励产生与覆盖评估.中国科学院研究生院博士学位论文.2006：83-103页
[151]沈海华,卫文丽,陈云霁.覆盖率驱动的随机测试生成技术综述.计算机辅助设计与图形学学报,2009,21(4)：419-431页
[152]丁谢THUASDSP2004处理器功能验证的设计及实现.电子科技大学硕士学位论文.2006：41-67页
[153]Prasad Joshi, Peter A. Beerel, Marly Roncken and Ivan Sutherland. Timing Verification of GasP Asynchronous Circuits:Predicted Delay Variations Observed by Experiment. Concurrency, Compositionality, and Correctness,2010,5930:260-276P
[154]Furumiya T, Ng DC, Yasuoka K, et al. Functional verification of pulse frequency modulation-based image sensor for retinal prosthesis by in vitro electrophysiological experiments using frog retina. Biosensors & Bioelectronics,2006,21(7):1059-1068P
[155]许庆国,缪淮扣.在原型验证系统中构建度量区间时序逻辑公式的时间自动机(英文)Journal of Shanghai University(English Edition),2008,12(04):339-346页