【摘 要】
：
高速铁路列控系统的安全与否直接涉及人民的生命财产安全,对高速铁路列控系统进行严格的形式化验证具有重要意义.但是随着高速铁路列控系统软件以及硬件规模的不断增大,系统
【机 构】
：
中国科学院软件研究所计算机科学国家重点实验室,北京交通大学轨道交通运行控制国家工程中心,北京交通大学轨道交通控制与安全国家重点实验室,
论文部分内容阅读
高速铁路列控系统的安全与否直接涉及人民的生命财产安全,对高速铁路列控系统进行严格的形式化验证具有重要意义.但是随着高速铁路列控系统软件以及硬件规模的不断增大,系统的复杂性有了很大的提高,直接对高速铁路列控系统进行形式化验证已经变得越来越困难.另一方面,由于图形化建模和仿真表现方式直观且易于理解,在工程实践中已经得到了广泛的应用.因此,为了更好地保证铁路系统的安全,对系统进行仿真,排除部分安全隐患显得尤为重要.本文通过使用Simulink/Stateflow建模工具对高速铁路列控系统的行车许可,等级升级及部分模式转换场景进行了建模.该模型具有普适性,通过修改参数信息,可以对不同的等级转换和模式转换的组合情况进行仿真.本文使用该模型对10种组合情况进行了仿真,发现在某些情况下可能会出现不正常停车或者等级转换失败的现象.类似于测试,仿真仅仅能够发现错误,如未发现错误,也不能证明系统是正确的.因为仿真的这种不完备性,对仿真辅助形式验证在安全攸关系统设计中非常必要.为此,取其中一个不正常停车的场景进行了形式验证,验证结果证明在任何情况下都不能正常停车.
其他文献
目的:分析应用软肝健脾胶囊治疗肝郁脾虚型乙肝肝硬化的疗效。方法:以门诊患者为主,收治乙肝肝硬化患者80例,随机分两组。对照组常规治疗,治疗组口服软肝健脾胶囊,2个月为1个
幸福作为人类的永恒追求,也是教育的终极目标。创新创业教育在推动人才培养范式深刻变革的同时,必须回答"教育如何与人的幸福"相关涉的问题,以提升人的教育获得感和幸福感。
在我国高校行政管理工作之中,绩效管理是其中的核心重点组成部分。通过一个有效的绩效管理体系能够有效促进高校的资源配置以及目标协调。因此,绩效管理工作对于高校来说具备
本文针对景德镇资源枯竭型城市人才不足的实际,对江西陶瓷工艺美术职业技术学院现代化学徒制人才培养实证研究成果《陶瓷类专业人才培养要体现"工"与"艺"结合的人才培养模式
新媒体是把＂双刃剑＂,人们在享受其带来的便利的同时,也因依赖过度而沉迷,青少年更是如此。过度接触新媒体及其不当内容导致缺乏独立思考、理性认知消解、自我迷失、价值观扭曲,
一条路上的货车调度问题是线上的在线服务器问题的推广．决策者必须以在线方式做出决策，即已知现在和过去的信息而对未来一无所知情况下决策如何调度货车完成服务需求．优化目标是
党中央在十九大提出了办好继续教育的新任务,新时代继续教育呈现人民日益增长的终身学习需要和继续教育不平衡不充分发展之间的矛盾。如何认识和解决新时代继续教育的主要矛
园林花卉是构建园林工程技术专业知识体系的一门骨干课程，但在教学中存在实践课时少，理论课时相对较多；教学内容与花卉生产实践结合不够紧密；教学方法和教学手段单一等问题。针对
1病例资料患儿,男,9岁。以发现心肌酶升高20天为主诉就诊于我院。缘于20天前患儿因腹泻、腹痛于当地医院行心肌酶检查发现心肌酶升高(具体数值不详),予以静点营养心肌药物20
ue＊M＃’＃dkB4＃＃8＃”专利申请号:00109“7公开号:1278062申请日:00.06.23公开日:00.12.27申请人地址:（100084川C京市海淀区清华园申请人:清华大学发明人:隋森芳文摘:本发明属于生物技