原文传递
列车自动防护系统的形式化建模与验证
| 论文题名： | 列车自动防护系统的形式化建模与验证 |
| 关键词： | 时间自动机;列车自动防护系统;模型验证;安全制动曲线;UPPAAL |
| 摘要： | 列车自动防护(ATP)系统是列车运行控制系统的核心子系统，系统的安全性和可靠性直接关系到列车的运行安全。ATP系统作为典型的、复杂的安全苛求实时系统，系统功能复杂，系统内部相互通信频繁，对实时性有很高的要求。系统既要求逻辑运算结果是正确的，又要求必须在规定的时间限制内产生结果。如何保证开发的ATP系统功能与系统需求规范的一致性，进而保证系统的正确性和安全性成为研究人员亟待解决的问题。 形式化方法是以严格的数学理论为基础，可以对系统需求规范进行准确的描述，避免了自然语言的随意性，能够很好地解决上述问题。本文在对形式化方法进行分析和比较的基础上，选择时间自动机理论描述实时并发系统功能流程。以ATP系统为例对时间自动机进行详细的分析，研究了构建系统时间自动机网络模型的方法，并对UPPAAL这种行为模型验证工具进行了详细的研究。 论文以轨道交通列车自动防护系统为研究对象，对系统的功能进行详细的分析，着重研究了系统的速度监督与超速防护功能以及同步功能。针对系统功能需求，采用UPPAAL模型验证工具对超速防护和同步功能流程进行形式化建模，并对模型的安全性和受限活性进行验证。通过验证，证明了模型功能与系统需求的一致性，表明使用时间自动机对ATP系统流程进行建模和分析，是保障ATP系统功能正确性和安全性非常重要的途径。论文用VC6.0软件工具对车载ATP速度防护模型进行了设计与仿真，实现了车载ATP的速度监督与超速防护功能。 |
| 作者： | 蒋建军 |
| 专业： | 交通运输工程 |
| 导师： | 王长林 |
| 授予学位： | 硕士 |
| 授予学位单位： | 西南交通大学 |
| 学位年度： | 2014 |
| 正文语种： | 中文 |
检索历史
应用推荐
