毕业答辩--基于UPPAAL的列控系统的仿真验证.ppt

南,交,通,大,学,西,西南交通大学,基于UPPAAL的C2/C3列控系统切换仿真验证,西南交通大学2014届本科生学位论文答辩,日期：2014年6月21日,组织结构,形式化方法和UPPAAL的介绍,绪论,致谢,列控系统及其等级转换过程分析,C2/C3等级转换过程建模和验证,结论和展望,第一章绪论,研究背景：中国是世界上人口数最多的国家，人口流动量大。国家制定了我国长期铁路网发展规划。CTCS是我国自主研发并且适合我国国情的列控系统,研究意义：在列控系统的设计过程中，及时发现设计的缺陷，保证列控系统的安全性。,研究问题：CTCS2/CTCS3等级转换的验证,5,1.2我国铁路网规划,精河-伊宁铁路210km,中吉乌铁路160km,阿勒泰至奎屯线550km,青新线1240km,龙岗至格尔木线630km,太原至中卫(银川)线720km,西平线300km,哈密至临河线1450km,兰州（西宁）至重庆（成都）铁路900km,隆黄铁路430km,中缅铁路620km,柳州肇庆铁路410km,中老铁路750km,新建昆河铁路380km,成昆复线1110km,皖赣复线520km,南昆复线660km,渝怀复线580km,宁西线西合复线950km,京哈客运专线1860km含：北京至哈尔滨1230km；天津至秦皇岛260km;沈阳至大连1160km,杭州-宁波-深圳客运专线1600km,浙赣客运专线880km,南京-武汉-重庆-成都客运专线1900km,徐州至兰州客运专线1400km,京广客运专线2230km,京沪客运专线1300km,青岛-太原客运专线770km,皖赣复线520km,包西复线920km,包西线西段复线600km兰青复线190km青藏线西格段复线810km,吐鲁番库尔勒复线480km,兰新线乌阿段复线450km,列控系统发展史,地面人工信号,地面自动信号,机车信号,自动停车,速度自动防护,自动驾驶,第二章形式化方法和UPPAAL,形式化方式：形式化方法是用于规范、设计与验证并且基于数学的计算机验证方法，包括了多种语言、技术与工具。,UPPAAL:UPPAAL是由Aalborg大学和Uppsala大学联合开发的一个基于时间自动机的验证工具，其用户界面包括3部分:系统编辑器，模拟器和验证器验证。,为什么选择形式化方法？形式化的方法解决了复杂系统在设计阶段所隐藏的问题，这样的做法就能极大的减少软件开发的风险。,位置：原始位置，约束位置，紧急位置,通道：广播通道，紧迫通道,第三章列控系统及其等级转换流程分析,列控系统的组成,C3进入C2的过程分析,CTCS2工作原理,CTCS3工作原理,C2进入C3的过程分析,1,2,3,4,5,CTCS分级,CTCS0/1：由通用机车信号和安全型运行监控记录装置。,CTCS2：基于应答器和轨道电路信息传输，机车乘务员凭机车信号行车。,200km/h速度250km/h,CTCS3：基于无线信息输，机车乘务员凭车载信号行车。,300km/h速度350km/h,CTCS4:基于无线通信传输平台，取消轨道电路，实现虚拟闭塞或移动闭塞。,速度160km/h,CTCS组成,总体分为：地面子系统+车载子系统CTCS0：通用机车信号+列车运行监控记录装置CTCS1：（轨道电路+点式信息设备）+（主体机车信号+点式信息接收模块+安全型运行监控记录装置）CTCS2：(列控中心)+（连续信息接收模块+测速模块+车载安全计算机+人机界面）CTCS3:（无线闭塞中心+无线通信地面设备）+C2车载+(GSM-R无线电台和信息接收模块）CTCS4：CTCS3+取消轨道电路,车站列控中心,轨道电路,LEU,车站联锁,CTCS-2级系统框图,CTCS2系统结构图及功能,微机监测,车站列控中心,微机联锁,轨道电路,车务终端,车站联锁,LEU,记录器,制动器,BTM,STM,车载安全计算机,人机界面,BTM天线,STM天线,地面应答器,14,LEU,联锁,CTCS2,轨道占用检测,CTCS2,16,无线闭塞,应答器,联锁,Eurocab,CTCSlevel3,GSM-R,轨道占用检测,CTCS3系统结构图及功能,17,场景3：C2进入C3动画演示,分界点,预告应答器,转换应答器,等级转换预告信息,立即执行等级转换,C3与C2边界的无线电场强覆盖,返回,18,分界点,预告应答器,切换应答器,等级转换预告信息,立即执行等级转换,场景3：C3进入C2动画演示,C3与C2边界的无线电场强覆盖,返回,第四章C2/C3等级转换过程建模和验证,建模过程,各个模型之间的信息流,对各个对象建立模型,模拟验证,各个功能分析验证,1,2,3,4,预告应答器通知准备等级转换,通知司机到达转换区域,司机确认,建立与RBC链接,建立链接建立通信,确认,向RBC发送数据,消息129,RBC确认列车数据,消息8,列车经过等级转换执行点,执行转换，进入C3区域,车载向RBC报告新等级和位置,消息136,确认,司机,车载设备,RBC,利用UPPAAL进行建模和验证,第五章结论和展望,成功利用UPPAAL对C2/C3的切换进行建模和验证。通过在列控系统设计阶段，对C2/C3的切换进行建模和验证，保证了列控系统的安全性，但是并没有考虑转换失败时如何进行处理，这是本次设计的缺陷。,大学本科的学习生活即将结束。在