原文传递
铁路信号系统中联锁软件形式化描述方法的研究
| 论文题名： | 铁路信号系统中联锁软件形式化描述方法的研究 |
| 关键词： | 铁路信号;时间自动机;联锁软件;软件开发 |
| 摘要： | 铁路联锁软件是一种典型的安全性软件,其失效可能会带来大批生命财产的损失或严重的环境破坏.在目前通用的软件开发方法中,其描述通常是用非形式化的图和文本,不能描述系统期望的存在于构件之间的接口,不能描述不同的组成系统的组合关系,难以被开发人员理解,更不能用来分析其一致性和完整性等特性.采用形式化方法为铁路联锁软件规则建模可以成为解决以上问题的入手点,在保证软件安全性和可靠性方面,也有很重要的意义. 本文的研究对象是由合肥工业大学开发的"HJ04A铁路信号计算机联锁系统".其主要内容是对联锁软件规则进行形式化描述并进行比较分析,找到更适合描述联锁软件规则的形式化方法,即时间自动机,利用UPPAAL实时验证工具进行建模和验证. 论文在充分了解了计算机联锁软件的背景和现状的情况下,提出了形式化方法在铁路信号系统联锁软件需求分析阶段具有重要的作用.然后介绍了形式化方法的概念和几种常见的形式化方法的定义和原理,接着介绍了铁路信号的相关概念、计算机联锁软件规则,并利用UML和Petri网两种模型分别对联锁软件规则进行形式化描述,分析其优缺点,提出时间自动机模型是一种更适合联锁软件规则建模的模型.最后主要介绍了基于时间自动机的一种实时自动验证工具UPPAAL,并且利用UPPAAL的集成环境对联锁软件规则进行建模和验证. |
| 作者： | 张华 |
| 专业： | 计算机应用与技术 |
| 导师： | 魏臻 |
| 授予学位： | 硕士 |
| 授予学位单位： | 合肥工业大学 |
| 学位年度： | 2007 |
| 正文语种： | 中文 |
检索历史
应用推荐
