UML活动图的正确性检测

摘要

UML(统一建模语言)活动图广泛用于软件开发过程,然而它是半形式化的模型,不能进行推理,无法保证其正确性.为了保证它的正确性,必须先把它转化为形式化模型再进行检测.现有工作已将活动图转换成变迁系统、进程代数、Petri网等模型,需要增加或丢失大量信息.本文提出一种新的方法,该方法直接将活动图转换成被称为依赖结构的形式化模型,不会增加或减少活动图的任何信息.基于依赖结构模型我们首先讨论了检测活动图的正确性方法,然后介绍相应的工具;最后用一个实例来详细说明检测过程.该工作有助于软件工程师正确地使用UML活动图对软件系统进行分析和设计.