不确定环境下可信国产城轨控制系统（iCMTCt）构造关键技术研究

CBTC (Communication Based Train Control) is becoming a mainstream technology in the development of contemporary subway signal system in China. Since subway trains are running in an uncertain environment (e.g., unreliable communication channels, device variations, etc.), when developing CTBC software, various uncertain factors should be considered. Consequently, it’s a big challege for CBTC venders to guarantee the trustworthiness of CBTC systems. ..The objective of this project is to facilitate the trustworthy construction of the iCMTC (Intelligent Communication-based Moving-block Train Control), which is a domestic CBTC system developed by Casco Ltd. To effectively reduce the iCMTC construction time while guarantee the trustworthiness, this project will investigate new methodologies as well as new formal techniques to improve the current top-down design flow of the iCMTC, which is adopted by Casco Ltd. By focusing on the the modeling, synthesis, simualtion and verification, this project will mainly study the following four issues: 1) How to formally model, verify and evalute the requirements of iCMTC systems in an uncertain environment? This project will try to develop new formal requirement specifications and models to address the ambiguity of the current natural language-based approaches. 2) How to efficiently reduce the complexity of current formal verification approaches? This project will try to avoid the “state space explosion” problem in practical iCMTC verification cases. 3) How to enable the quantitative evaluation and automated synthesis for iCMTC systems in an uncertain environment? This project will utilize statistical model checking based techniques to promote the quality of derived models and develop promising optimization methods to reduce the overall synthesis time. 4) How to guarantee the consistency between different abstraction levels? This project will figure out how to reuse the validation efforts across different abstraction levels to reduce the overall validation efforts. ..By exploring various efficient and effective formal modeling, synthesis and formal verification techniques, we believe that the outcomes of this project can not only significantly reduce the CBTC construction time, but also can enhance the performance, reliability and predictability of constructed CBTC systems. By integrating all the investigated techniques together, a tool chain will be formed which can enable the development of the new generation of the trustworthy iCMTC system, named iCMTCt.

基于通信的列车控制系统(CBTC)已成为城市轨道交通信号选型主流制式。由于网络通信与设备差异导致CBTC软件运行时存在多种不确定因素，使得如何保证CBTC系统的可信是一个具有挑战性的难题。本项目围绕我国自主产权CBTC系统iCMTC的可信构造，探索如何采用多种优化方法与技术，实现不确定环境下iCMTC系统设计、综合，仿真与验证。主要研究不确定情况下iCMTC系统需求的形式化建模、验证与评估方法，避免需求描述的二义性，提高需求模型的功能与非功能可信；研究设计模型的高效形式化验证方法与技术，提高形式化验证的效率；研究不确定环境下模型的定量评估与自动化综合技术，降低精化过程的时间，提高自动化生成模型的质量；研究不同抽象层次验证结果重用与一致性维护技术，在降低系统总体验证时间的同时保证设计与实现的一致。本项目还将开发工具链，支持iCMTC一体化可信开发，实现新一代增强版的可信iCMTCt。

CBTC是我国城市轨道交通信号选型主流制式。由于处于开放的不确定物理环境，如何保证CBTC系统的可信是一个极具挑战性的任务。本项目围绕不确定环境下自主产权CBTC系统iCMTC的可信构造，探索其高效设计、综合、仿真与验证的方法与技术，降低自顶向下iCMTC系统可信构造的总体时间与复杂度。本项目主要研究内容与贡献如下:..1. 高阶规约建模与定量评估。创新地提出了面向iCMTC高阶规约建模的描述语言Hybrid Lustre，支持在系统级对iCMTC系统与连续物理环境实施协同建模。基于AADL语言与统计模型检验技术设计定量评估框架，支持不确定环境下iCMTC体系架构的评估与寻优。创新地提出了iCMTC的形式化需求模型分析方法，能够有效检测需求描述的二义性与功能描述错误。..2. 设计模型的建模、评估与验证。结合混成自动机，扩展建模规范MARTE建立混成系统通信模型，支持包括车载定位系统等在内的多个iCMTC子系统的连续行为建模。基于价格时间自动机与监督学习技术，建立了不确定环境下iCMTC系统的形式化建模与定量评估框架，支持不确定环境下自动列车驾驶子系统ATO的设计优化。..3.基于分支界定方法，研究不确定与资源受限情况下设计规约与模型的高效综合，降低精化时间并提高生成模型的质量。创新地提出了两阶段裁剪与结构感知的并行裁剪方法，支持资源分配与调度方案的快速寻优。实验结果显示，我们提出的方法比现有最好的分支界定方法快10-1000倍。..4.底层实现的测试与一致性保障。研发了半自动分析工具CASDL，支持自动分析需求中的变量并生成测试用例，能够在降低系统的总体测试时间（80%优化）的同时保证设计与实现的一致。基于下推系统创新地提出了支持程序API使用的模型检测方法，支持底层程序API错误的高效检测。..本项目开发的原型工具链目前已初步应用于实际的iCMTC构造流程。实验结果显示，我们的方法能够在缩短iCMTC系统开发周期的同时，保证不确定环境下iCMTC系统高可信。