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

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

项目编号： No.91418203

项目类型： 重大研究计划

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 陈铭松

作者单位： 华东师范大学

项目金额： 150万元

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

英文关键词： Communication Based Train Control；Trustworthy Construction；Uncertain Environment；Formal Verification；Quantitative Evaluation