通用无线通信列控系统的形式化建模与分析

The general purpose radio communication based train control systems will be the main trends for inter-city and light rail transit systems. In the development of these software systems, system specification, which is usually written in a natural language, is the foundation of the software system. Because of the lack of rigorous theory regarding natural language and its ambiguities, the system dependability and safety are seriously imperiled. Regarding these problems, in order to guarantee the software quality of a railway system by analyzing its specification, this research project will be implemented as follows: firstly, the relationship between discrete events and continuous state-flow in system operation based on Markov theory will be investigated, and then the hybrid models according to the transition between them will be established. This will be followed by the determination of system parameters and the analysis of reachability and equivalence between hybrid models. Secondly, multi-level and multi-angle graphical models to express overall system structure and the relationship between modules will be established, and then the completeness and reasonableness of system structure and function will be examined. Thirdly, functional requirements specification (FRS) using VDM++ will be described. Lastly, the internal consistency of FRS by transforming the concrete VDM++ model into a HOL (higher order logic) model to discharge the proof obligations will be verified, and the satisfiability will be validated by executing the formal specification. This is fundamental and perspective research which will provide theoretical basis for guaranteeing the system's safety and dependability.

基于通用无线通信的列控系统是未来开发城际铁路或轻轨交通系统的主要信号系统之一。然而，采用自然语言编写的规格说明作为软件系统的根本，因其二义性及严密分析理论的缺乏，严重影响着系统的稳定性及安全性。为从源头保障列控软件系统的质量，本课题将开展如下研究：基于马尔可夫理论研究系统运行时的事件发生和状态变化，建立连续状态和离散事件相互转移的精确混杂模型，确定系统参数，并分析系统动作的可达到性、等效性等特征；通过建立多层次、多角度的可视化系统模型来展示系统的整体结构和模块关联关系，并验证系统结构和功能的完整性及合理性；采用面向对象的形式化方法来精确的描述系统的函数功能需求；最后将形式化模型转化为高阶逻辑的模型，以实现系统内部一致性的证明。本研究具有前瞻性，属应用基础研究课题，将为确保软件系统的安全性和稳定性提供理论基础。

基于通用无线通信的列控系统是未来开发城际铁路或轻轨交通系统的主要信号系统之一。然而，采用自然语言编写的规格说明作为软件系统的根本，因其二义性及严密分析理论的缺乏，严重影响着系统的稳定性及安全性。为从源头保障列控软件系统的质量，为确保无线列车控制系统的可靠性和安全性， 在“基于无线通信列车控制系统的形式化建模与分析”国家自然科学基金的资助下，针对传统的基于测试的方法难以保障列控系统安全的问题，围绕轨道交通系统模型建立与安全保障问题，完成了预定的研究目标，主要成果如下：.建立了适合描述无线列控系统运动过程的混杂系统建模与分析理论，增强了对高速列车系统机理的分析；并且针对混杂系统中，参数化非线性系统模型，提出了模型参数辨识和状态估计理论与方法；.建立了基于UML(Unified Modeling Language)的无线列控系统的图形化模型，实现了系统结构合理性和完整性的检验；.基于完成了图形化系统模型和混杂模型与形式化模型的转换，确保了形式化模型与自然语言描述系统规约的一致性；针对面向对象的形式化模型，实现了内部一致性的自动形式化验证；最终为无线列控系统建立完整的形式化建模与分析理论。该研究工作扩展了VDM++ (Vienna Development Method)形式化方法的局限；并充分利用混杂自动机和UML的图像化表达，增强了形式化模型的外部一致性，提高了系统设计的可靠性。.本研究具有前瞻性，属于应用基础研究范畴，将为确保软件系统的安全性和稳定性提供理论基础。.