论文摘要
随着计算机技术的飞速发展,软件系统的广泛应用,软件系统间的可移植性、协同工作能力和可维护性问题日益突出,以模型为软件开发关键的模型驱动架构MDA方法是解决这些问题而产生的新技术。用UML活动图建立MDA中的平台无关模型PIM是模型的核心之一。但是很多模型在建模过程中缺乏正确性验证或仅进行局部的语法检验,造成模型存在死锁、活锁等缺陷,这直接引发了模型执行过程中的诸多问题,如任务不能完成、超期完成等。因而,在建模阶段验证模型的正确性就显得尤为重要。在国家863项目“模型驱动式高可信软件开发技术”(编号:2006AA01Z165)的支持下,我作为小组成员实现了对UML活动图的自动化验证。模型检测作为形式化验证模型的方法,有着自动化和提供反例等诸多优点。并且近年在UML模型中得到广泛应用。模型检测器SPIN是由贝尔实验室开发的一种专门用于软件验证的工具。本文基于模型检测工具SPIN,对UML活动图建立的PIM模型进行形式化分析和验证,并对UML活动图进行动态模拟。首先在UML活动图建立的PIM模型基础上,将UML活动图转化为模型验证工具SPIN能够识别的PROMELA语言模型,然后结合SPIN的验证功能对活动图进行验证,给出验证信息,并且在出错的情况下可以对活动图进行动态模拟。
论文目录
相关论文文献
- [1].活动图集[J]. 辅导员 2016(02)
- [2].人脑活动图将解开思维奥秘[J]. 百科知识 2013(07)
- [3].好奇好学 动手动脑 学会发现 开启智慧[J]. 小学生导刊(高年级) 2015(Z1)
- [4].基于形式活动图的协议一致性测试用例生成方法研究[J]. 安徽大学学报(自然科学版) 2013(03)
- [5].基于资源扩展活动图的并发测试用例生成方法[J]. 航天控制 2019(01)
- [6].可视化教学过程设计研究[J]. 中国电化教育 2009(03)
- [7].一种基于UML类图和活动图的故障树生成方法[J]. 计算机科学 2016(07)
- [8].基于新活动演算的SysML活动图形式化描述[J]. 计算机应用与软件 2015(10)
- [9].UML活动图的一种逻辑语义[J]. 福建师范大学学报(自然科学版) 2010(03)
- [10].基于UML活动图模型的测试用例设计[J]. 现代计算机(专业版) 2009(07)
- [11].UML活动图的正确性检测[J]. 软件工程 2018(03)
- [12].基于故障扩展SysML活动图的软件安全性分析方法研究[J]. 小型微型计算机系统 2015(09)
- [13].循环嵌套结构的测试场景反蚁群自动生成方法[J]. 小型微型计算机系统 2012(08)
- [14].基于UML活动图的系统测试方法研究[J]. 计算机应用与软件 2010(12)
- [15].基于UML活动图的测试研究进展[J]. 计算机科学 2008(02)
- [16].基于UML活动图模型测试场景自动生成的优化[J]. 电子设计工程 2019(24)
- [17].一种基于故障扩展SysML活动图的安全性验证框架研究[J]. 计算机科学 2015(07)
- [18].黄南州图书馆开展文化系列活动图锦[J]. 图书馆工作与研究 2019(09)
- [19].一种基于UML活动图的切片方法[J]. 微计算机信息 2009(18)
- [20].基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究[J]. 小型微型计算机系统 2015(03)
- [21].一种基于SysML活动图的风险识别方法[J]. 数字技术与应用 2020(07)
- [22].第17届黄河旅游节主要活动图集[J]. 公关世界 2011(10)
- [23].“人物分布图”和“人物活动图”教学浅析[J]. 中学历史教学参考 2019(15)
- [24].改进的UML活动图在建模中的研究与实现[J]. 电子科技大学学报 2009(01)
- [25].基于扩展UML活动图的过程建模[J]. 计算机应用 2009(03)
- [26].基于蚁群算法UML活动图的测试用例生成研究[J]. 泰州职业技术学院学报 2010(05)
- [27].赛场外的赛场 乒乓外的乒乓——世乒赛期间重要活动图集[J]. 乒乓世界 2008(04)
- [28].UML活动图到时间Petri网的映射方法[J]. 电子科技 2012(02)
- [29].UML活动图到Petri网映射方法的研究与实现[J]. 微计算机信息 2009(06)
- [30].基于WF Flowchart的UML活动图动态构建与测试[J]. 软件 2018(05)