【作者】 刘铭；

【导师】 张国印；

【作者基本信息】 哈尔滨工程大学 ， 计算机应用技术， 2011， 博士

【摘要】 随着现场总线技术、计算机网络通信技术、嵌入式系统控制技术以及故障诊断技术的快速发展,现代列车控制系统已经从孤立的数字控制系统发展成为基于网络的分布式控制系统。列车通信网络系统应用总线技术对分布于列车上的设备进行控制,属于一种专用的混合分布式实时系统。随着我国铁路客运进入高速时代,列车通信网络系统的自主研发、设备制造、维护运营等问题成为近年的研究热点。近来,列车通信网络系统研究不断深入,在取得许多成果的同时,有些问题在系统设计过程中变得日益突出,如列车通信网络系统的形式化描述问题、符合列车通信网络标准的行为一致性验证问题等。本文以解决这些问题为目标,以面向应用为出发点,对列车通信网络系统的形式化建模、静态属性分析、动态属性验证和模拟验证等关键技术进行了研究。本文首先对基于形式化方法和模拟方法的列车系统建模及验证的相关研究进行了综述,以列车系统的设计和验证流程为主线,从列车通信网络标准的分类、列车通信网络系统的形式化建模、动态属性验证、模拟验证等方面进行了研究,总结了该领域存在的问题和下一步的研究方向。综合运用形式化语义、数学理论分析、模型检查和模拟验证技术,提出了一种适用于列车通信网络系统的形式化建模和验证方法,为列车通信网络系统的设计和验证提供了系统级的解决方案。深入分析了IEC61375列车通信网络协议,将列车通信网络建模划分为网络拓扑结构和网络功能节点建模两部分工作,提出了一种分层次的列车通信网络系统形式化建模方法,为了满足建模需求,对Petri网进行扩展得到层次实时有色Petri网,建立了完整的列车通信网络系统模型,验证了形式化建模方法的有效性。以列车通信网络标准和系统特征为依据,定义了列车通信网络系统的HRTCPN模型的静态属性,并以线性代数、图论等数学方法为基础提出了静态属性的检测规则。此外,基于关联矩阵和S-不变量运算对系统模型的实时性分析进行了研究,提出了一种系统时间参数的评估方法和系统实时性能优化方案。针对已有方法在列车通信系统动态属性验证方面存在的完整性问题,提出了一种系统模型的形式化验证方法,以时间自动机模型和符号模型检查理论为基础,设计了HRTCPN模型到形式化验证输入语义的转换规则,并且基于假设／保证组合检查策略提出了系统的分解方法和假设、保证规则、完整地提取了动态属性,有效避免了状态空间爆炸问题,提高了针对列车通信网络标准进行动态属性验证的完整性。列车通信网络系统协议大部分主要功能都在网络控制器中实现,对网络控制器的验证在某种意义上等同于系统协议实现级别的验证。基于高级验证方法学构造了列车通信网络控制器的模块级和系统级功能验证模型,设计了网络拓扑级验证模型,弥补了传统验证方法难以模拟通信过程的不足。提出了基于功能覆盖率的驱动测试生成方法、对多重覆盖率收集技术和组件重用技术进行了研究,优化了验证环境。根据列车通信网络标准和一致性测试标准设计了错误注入方法,解决了异常处理机制的验证问题,显著提高了验证的覆盖率和缺陷识别率。最后,总结论文工作,并提出了下一步的研究方向。更多还原

【Abstract】 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.更多还原