原文传递
实时状态图的形式化及其应用研究
| 论文题名： | 实时状态图的形式化及其应用研究 |
| 关键词： | 软件质量保证;状态图时间扩展;形式化;分散式铁路联锁系统 |
| 摘要： | 随着智能化时代的到来,计算机软件得到了广泛应用。然而在实际应用中,小到随身手机系统的频频崩溃,大到事关国计民生的铁路信号、飞行控制等系统的不时故障,问题频出。软件系统质量的保障一直以来都是国内外研究的重点及热点。需求说明是软件系统开发的基础和根本,因此对软件需求的全面准确把握极其重要。目前,统一建模语言UML已广泛应用于工业软件需求的建模分析,但是,在面对软件的非功能性需求以及时间苛求的软件系统时,UML因其自身缺陷难以应对。同时,UML是半形式化的,其模型设计的正确性无法得到验证,这必将为软件系统后续的开发埋下隐患。时间Petri网作为一种兼具严格的数学表示及便捷友好的图形化表达方式的形式化方法,已被成功应用于时间苛求系统的质量保障。因此,考虑到软件非功能性需求中的时间因素,为了更好的保证时间苛求系统的质量,本文提出了“基于时间Petri网的UML状态图的形式化方法”,根据此方法初步实现了时间扩展状态图模型到时间Petri网模型的自动转换工具timConvert。本论文的主要研究工作如下: 1.针对状态图建模分析应用的现状,为了更好的服务时间苛求系统,本文给出了基于时态区间的标准状态图的时间扩展方法: 2.在对时间扩展后的状态图进行分析之后,提出了时间扩展状态图的形式化定义,并完成了对时间扩展状态图主要建模元素,相关基本性质的形式化描述: 3.为验证时间扩展状态图建模结果,在分析和比对了时间扩展状态图和时间Petri网的语义及建模元素之后,提出了两者之间的映射规则; 4.基于上述研究成果,结合对具备数据交换功能的XML文档的研究,本文设计并实现了从时间扩展状态图模型到时间Petri网模型的自动转换工具timConvert: 5.以时间关键的复杂系统一分散式铁路联锁系统一为例,对本文所做的主要工作进行分析和验证。 论文结果表明,本文研究内容可有效完成对时间苛求系统中时间因素的建模分析及验证。 |
| 作者： | 赵凯 |
| 专业： | 计算机应用技术 |
| 导师： | 黑新宏 |
| 授予学位： | 硕士 |
| 授予学位单位： | 西安理工大学 |
| 学位年度： | 2014 |
| 正文语种： | 中文 |
检索历史
应用推荐
