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

批准号:
91418203
项目类别:
重大研究计划
资助金额:
150.0 万元
负责人:
陈铭松
依托单位:
学科分类:
F0203.软件理论、软件工程与服务
结题年份:
2016
批准年份:
2014
项目状态:
已结题
项目参与者:
周庭梁、陈小红、孙海英、Robert De Simone、Frederic Mallet、缪炜恺、宋富、张磊、陈祥
国基评审专家1V1指导 中标率高出同行96.8%
结合最新热点,提供专业选题建议
深度指导申报书撰写,确保创新可行
指导项目中标800+,快速提高中标率
微信扫码咨询
中文摘要
基于通信的列车控制系统(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 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系统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系统高可信。
期刊论文列表
专著列表
科研奖励列表
会议论文列表
专利列表
DOI:10.1155/2016/4149059
发表时间:2016-03
期刊:Mathematical Problems in Engineering
影响因子:--
作者:Guobin Wang;J. He;Jing Liu;Haiying Sun;Zuohua Ding;Miaomiao Zhang
通讯作者:Guobin Wang;J. He;Jing Liu;Haiying Sun;Zuohua Ding;Miaomiao Zhang
Efficient Resource Constrained Scheduling Using Parallel Two-Phase Branch-and-Bound Heuristics
使用并行两阶段分支定界启发法进行高效资源约束调度
DOI:10.1109/tpds.2016.2621768
发表时间:2017-05
期刊:IEEE Transactions on Parallel and Distributed Systems
影响因子:5.3
作者:Yongxiang Bao;Xin Fu;Geguang Pu;Tongquan Wei
通讯作者:Tongquan Wei
GPU-Based Fluid Motion Estimation Using Energy Constraint
使用能量约束的基于 GPU 的流体运动估计
DOI:10.1142/s0218126617500220
发表时间:2017-02
期刊:Journal of Circuits, Systems, and Computers
影响因子:--
作者:Siyuan Xu;Han Zhuang;Xin Fu;Junlong Zhou;Mingsong Chen
通讯作者:Mingsong Chen
DOI:--
发表时间:--
期刊:软件学报
影响因子:--
作者:陈铭松;鲍永翔;孙海英;缪炜恺;陈小红;周庭梁
通讯作者:周庭梁
DOI:10.1142/s0218126617500165
发表时间:2017
期刊:J. Circuits Syst. Comput.
影响因子:--
作者:Junlong Zhou;Min Yin;Zhifang Li;Kun Cao;Jianming Yan;Tongquan Wei;Mingsong Chen;Xin Fu
通讯作者:Junlong Zhou;Min Yin;Zhifang Li;Kun Cao;Jianming Yan;Tongquan Wei;Mingsong Chen;Xin Fu
云-端架构信息物理系统高效可信构造关键技术研究
- 批准号:--
- 项目类别:面上项目
- 资助金额:54万元
- 批准年份:2022
- 负责人:陈铭松
- 依托单位:
不确定环境下信息物理系统高效可信构造关键技术研究
- 批准号:61872147
- 项目类别:面上项目
- 资助金额:65.0万元
- 批准年份:2018
- 负责人:陈铭松
- 依托单位:
基于虚拟原型的信息物理融合系统高效可信构造研究
- 批准号:61672230
- 项目类别:面上项目
- 资助金额:16.0万元
- 批准年份:2016
- 负责人:陈铭松
- 依托单位:
基于高阶规约定向测试的异构系统验证研究
- 批准号:61202103
- 项目类别:青年科学基金项目
- 资助金额:25.0万元
- 批准年份:2012
- 负责人:陈铭松
- 依托单位:
国内基金
海外基金
