论文部分内容阅读
无线调车机车信号和监控系统能够实现站场机车或车列的自动跟踪,实现调车信号、调车进路、调车作业单等在机车显示器上实时显示,并结合列车监控装置实现了对调车作业的自动安全防护控制和作业数据记录。该系统的研制及应用,提高了调车作业的信息化和安全性,有效解决了调车安全防护问题:同时给安全管理提供了可靠的历史依据。
时间自动机是形式化描述实时系统的重要理论,UPPAAL作为基于时间自动机理论的实时系统建模分析和验证工具,可以用于系统的设计、仿真分析和验证。UPPAAL具有高效、快速、使用方便等特点,已得到比较广泛的应用。
随着系统不断地推广和应用,系统安全、可靠无误地运行至关重要,因此对系统性能的相关部分进行形式化建模验证,保证系统的安全性可靠性是十分有必要的。
本论文使用UPPAAL工具对系统的车地无线通信协议及系统功能两部分进行了建模、仿真,分析系统运行过程中的状态变化,并根据系统需求规范和约束,构造相应的性质表达式,对系统的可达性、安全性、活性进行验证。
经过验证,系统不存在死锁,且修改后的系统车地无线通信协议满足实时性、安全性要求,有效地实现了车载与地面信息的实时交互和共享,为系统正常运行奠定了基础;系统能够完成环境信息的采集及处理,机车的入网注册及退网注销,机车控制模式的正确切换等功能。