公开(公告)号：CN105955755A

公开(公告)日：2016-09-21

申请号：CN201610334262.0

申请日：2016-05-19

Applicant: 上海大学

Inventor： 高洪皓 ,  缪淮扣 ,  许杰品 ,  曾红卫 ,  开金宇

IPC: G06F9/44 ,  G06F9/45

CPC classification number: G06F8/34 ,  G06F8/40

Abstract: 本发明涉及一种基于状态图的代码化验证方法，包括步骤：1)用ArgoUML状态图描述目标软件需求，进行需求分析；2)将ArgoUML输出的文件作为提取目标，抽取其状态图描述文件；3)解析状态图描述文件，获取状态图的节点状态，迁移信息以及状态属性；4)根据获取的状态图的节点状态，迁移信息以及状态属性将ArgoUML状态图转化为目标NuSMV代码；5)自动抽取检验性质，以交互式方式供用户二次编辑；6)调用NuSMV检验器执行检验，返回校验性质是否被满足，如不满足，给出出错位置点并展示路径序列。与现有技术相比，本发明可实现边对软件需求建模边实现自动化验证，同时使得设计分析人员不用再关心如何编写复杂的NuSMV程序，这些转化将自动实现。