毕业答辩-基于UPPAAL的区域控制器功能建模与验证.ppt_第1页
毕业答辩-基于UPPAAL的区域控制器功能建模与验证.ppt_第2页
毕业答辩-基于UPPAAL的区域控制器功能建模与验证.ppt_第3页
毕业答辩-基于UPPAAL的区域控制器功能建模与验证.ppt_第4页
毕业答辩-基于UPPAAL的区域控制器功能建模与验证.ppt_第5页
已阅读5页，还剩11页未读， 继续免费阅读

下载本文档

版权说明：本文档由用户提供并上传，收益归属内容提供方，若内容存在侵权，请进行举报或认领

文档简介

毕业答辩,2019/12/6,基于UPPAAL的区域控制器建模与验证2010级铁道信指导老师：,目录,形式化方法与验证,绪论,基于UPPAAL区域控制器切换流程建模与验证,结论与展望,研究目的意义,1.四纵四横到八纵八横2.2011年“7.23甬温线特别重大铁路交通事故”3.区域控制器间切换的复杂性,论文思路,1.CBTC及区域控制器介绍2.什么是形式化验证？3.形式化验证的必要性及发展历史4.UPPAAL工具介绍5.区域控制器间切换建模与验证,CBTC及区域控制器介绍,1.CBTC介绍2.区域控制器介绍,什么是形式化验证,形式化方法是用于规范、设计与验证并且基于数学的计算机验证方法，包括了多种语言、技术与工具。,形式化验证的必要性,列控系统是一个庞大而复杂的系统。,形式化的数学证明是论证软件安全性的最充分甚至往往也是最有效的工具。,形式化方法与运用,（1）形式化规范（FormalSpecifition）方法1）描述顺序系统行为的形式规范方法2）描述并发系统行为的形式规范方法3）集成的形式规范方法（2）形式化验证（FormalVerifition）方法1）模型验证（Modelchecking）2）定理验证（Theoremproving）,形式化工具,（1）模型检验工具1）时序逻辑模型检验器：SMV与Spin2）行为一致性检验器：FormalCheck3）组合验证器：PVS（2）定理证明器：1）自动化推导工具2）证明检验器,时间自动机,是为了适应实时系统的验证需求，从而解决实时系统建模和验证而对自动机理论的扩展。TA提供了一种简单有效的方法描述带有时间因素的系统状态转换图，在实时系统的建模与验证提供了理论依据。,UPPAAL,UPPAAL由丹麦的Aalborg大学和瑞典的Uppsala大学在1995年共同开发的，一款具有世界先进水平的实时自动验证工具。它用于可以被描述为非确定的并行过程的积的系统。每个过程被描述成由有限控制结构、实数据时钟和变量组成的时间自动机，通过管道和变量互相通信。,区域控制器工作状态,ZC有四种工作状态，我们可以分为以下四种情况：1）列车预登录2）列车进入ZC控制3）ZC正式控制列车4）列车注销,MA计算,ZC与其他子系统的信息交互,VOBC车载控制器ATS列车自动监控子系统ZC区域控制器CI计算机联锁,结论与展望,1.了解了形式化验证理论与工具2.理清了区域控制器的信息交互关系3.为软件系统
人人文库> 全部分类> 毕业设计 > 毕业论文

温馨提示

  • 1. 本站所有资源如无特殊说明，都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等，如果需要附件，请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸，网页内容里面会有图纸预览，若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对用户上传分享的文档内容本身不做任何修改或编辑，并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容，请与我们联系，我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

最新文档

评论

0/150

提交评论