毕业答辩-车站信号控制系统的形式化建模与验证.ppt_第1页
毕业答辩-车站信号控制系统的形式化建模与验证.ppt_第2页
毕业答辩-车站信号控制系统的形式化建模与验证.ppt_第3页
毕业答辩-车站信号控制系统的形式化建模与验证.ppt_第4页
毕业答辩-车站信号控制系统的形式化建模与验证.ppt_第5页
已阅读5页，还剩11页未读， 继续免费阅读

下载本文档

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

文档简介

车站信号控制系统的形式化建模与验证,计算机与通信工程系铁道信号2班学位申请人：指导老师：,2014届本科毕业设计（论文）答辩,内容概述,1,绪论,全电子计算机联锁,电子开关技术,自动控制技术,通信技术,故障安全,设计缺陷,形式化方法,车站信号控制系统的形式化建模与验证,2,绪论,研究现状：以其中两篇论文为例王观宁.基于UPPAAL的联锁进路控制流程建模与验证D.北京交通大学硕士学位论文.2009（无站场）黄菊.基于时间自动机的分散控制联锁系统建模与验证D.西南交通大学硕士学位论文.2013（一条进路)我的论文：全站建模与验证（包含站内所有进路）,3,形式化方法与UPPAAL,形式化方法：是一种基于数学的特种技术，如果一个系统有良好的数学基础，那么他就是可形式化的。Uppaal：是由瑞典Uppsala大学和丹麦Aalborg大学联合开发的一款基于时间自动机的形式化验证工具。,8,形式化方法与UPPAAL,时间自动机时钟约束：时钟解释：给一个时钟集合中的每一个时钟变量按照一定的映射关系重新赋值。,9,联锁与进路选排,联锁概念：,相互联系相互制约,保证站内行车安全,目的,信号机,道岔,轨道电路,4,联锁与进路选排,设计站场,简易平面布置图,5,联锁与进路选排,2、道岔处于解锁状态,1、轨道处于空闲状态,3、敌对进路未建立,选路条件检查,6,联锁与进路选排,控制流程,空闲,进路命令,查找进路号,开放信号,相备关是室否外占设用,信否号开是放,选路结束,敌是对否信开号放,是此否进有路,解除设备占用,Y,Y,Y,Y,N,N,N,N,7,建模与验证,建模本次设计中共建立8个模型，各模型联系右图所示：,Controller/中央控制器,SIgnalerMode/信号机电子模块,BlockMode/轨道电子模块,SwitchMode/道岔电子模块,SIgnaler/信号机,Block/轨道,Switch/道岔,Button/按钮,10,建模与验证,验证,1、逻辑功能验证,3、安全性验证,2、时间特性验证,11,程序解释,12,总结与展望,总结,自创利用Struct结构体建立软件内部联锁表,自设计进路表，与联锁表一起实现进路选排时数据查询的功能,通用性强，只需适当改编进路表和联锁表即可适应任何车站,首次结合具体站场，且对全站进行建模,所有验证性质均通过，充分说明了所建模型的正确性,13,总结与展望,不足与展望,程序运行时占用内存太多,程序中只实现了进路选排的基本功能,后续设计者可加入列车模型建立随机解锁过
人人文库> 全部分类> 毕业设计 > 毕业论文

温馨提示

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

最新文档

评论

0/150

提交评论