文档介绍：劣参未交癌乞≯一硕士学位论文基于时间自动机模型的系统安全计算机平台的形式化验证作者:郭志良导师:郜春海北京交通大学年
导师虢耐冬谚“签字日期:年月日氏签字日期:础,口年『、使用学位论文的规定。特授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索,并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国家有关部门或机构送交论文的复印件和磁盘。C艿难宦畚脑诮饷芎笫视帽臼谌ㄋ得学位论文作者签名:,
北京交通大学.,硕士学位论文基于时间自动机模型的系统安全计算机平台的形式化验证学科专业:交通信息工程及控制研究方向:运输自动化与控制年月作者姓名:郭志良导师姓名:郜春海学位类别:工学学号:职称:副教授学位级别:硕士学校代码:中图分类号:密级:公开
致谢首先感谢我的导师郜春海教授,两年多来给予我多方面的指导,让我在科研能力提升上获益匪浅。本论文的工作是在我的导师郜春海教授的悉心指导下完成的,郜老师敏锐的专业洞察力,让我可以接触到专业领域最前沿的学术动态,并帮助我很好地把握了论文的方向,掌握了科学的课题思考方式。谨在此再次表达我对郜老师的敬佩与感激之情其次,感谢马连川教授在实验室课题研究上的具体指导,让我在项目经验及专业技能上都收获颇丰。马连川教授渊博的学识及执著的钻研精神,都令人深深地为之折服。还有,王悉老师、袁彬彬师兄悉心传授各种工具的使用方法,帮助我很快熟悉项目的开展工作,在此深表谢意。同时,感谢在论文撰写期间,给予我关心和帮助的尹南、邓昌琪、修桂生、王超琦、张友兵、司继渊、刘海旭等同学。正是大家的相互支持,才得以更加顺利地完成论文的撰写。值此即将毕业之际,感谢交大六年多以来对我的培养,这是我人生中极为重要的一段时光,为我今后的继续成长奠定了基石。最后,将我的论文献给我的父亲母亲以及爷爷奶奶,正是心中一直怀有的对他们的感恩之情,让我在最困难的时候,能坚持前行。▲
中文摘要中又捅要摘要:众多工业控制领域要求其计算机控制系统具有高可靠、高可用和高安全的运行基础。安全计算机系统常用于军事、航空航天、工业控制、银行、通信等安全苛求甤领域,以避免由于计算机的失效造成重大事故。基于通信的列车运行控制瓸珻系统是当今世界列车运行控制系统的发展趋势,各主要发达国家都相继开发出自己的系统。在系统中,地面区域控制中心的主要组成部分是区域控制器以及数据存储单元渲衂芟角蛑兴辛谐档某翟乜刂破鱒列车所在位置和速度等信息发到安全计算机平台之上的应用程序中,经过保证安全的计算后再将移动授权发往控制列车的下一步运行,而酉统包括了其它列车控制子系统使用的所有数据库和配置文件,它的应用软件也需要搭建在安全计算机平台之上。二乘二取二冗余结构的安全计算机平台是提高系统安全性、可靠性的一种重要解决方式。列控系统的安全计算机平台采用二乘二取二冗余结构,它是一个实时系统,控制过程需要考虑时间因素。本文分析系统安全计算机平台系统的组成结构,提取出系统的功能约束,具建立系统的自动机网络模型,时性、安全性要求。采用基于时间自动机理论的建模验证工进行仿真分析,验证系统的功能性、实关键词:实时系统;安全计算机;时间自动机;模型验证;分类号:,、
瞄狟,,.琣.,琲琤,甅’甌:,—疭....猳’—ぁ甌、,
骸巍訡甶目录自动验证工具n诺亍中文摘要⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。引言⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.研究背景和对象⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.踩ḿ扑慊谕庋芯肯肿础璴系统安全计算机平台⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.问交椒ǖ囊搿研究内容⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯本文的组织结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯时间自动机及其验证工具⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.时间自动机理论⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯的构成与特点⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯需求规范语言⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.安全计算机平台系统的结构与功能分析⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯系统结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.各组成模块的功能⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.二取二功能的实现⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。.《南低辰峁埂.《ǖ赖墓ぷ髂J健.《闹饕9δ堋数据比较的实现⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。任务同步的实现⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..对二取二通道的安全控制⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..二乘功能的实现⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.礁鐾ǖ赖氖淙胍恢滦钥刂