| 摘 要: UML(统一建模语言)活动图广泛用于软件开发过程，然而它是半形式化的模型，不能进行推理，无法保 证其正确性。为了保证它的正确性，必须先把它转化为形式化模型再进行检测。现有工作已将活动图转换成变迁系统、 进程代数、Petri网等模型，需要增加或丢失大量信息。本文提出一种新的方法，该方法直接将活动图转换成被称为依赖 结构的形式化模型，不会增加或减少活动图的任何信息。基于依赖结构模型我们首先讨论了检测活动图的正确性方法， 然后介绍相应的工具；最后用一个实例来详细说明检测过程。该工作有助于软件工程师正确地使用UML活动图对软件 系统进行分析和设计。 |
| 关键词: 活动图；形式化模型；正确性 |
|
中图分类号: TP311.5
文献标识码: A
|
| 基金项目: 国家自然基金（61772004）；国家自然基金（61361136002）；福建省自然基金（2018J01777）. |
|
| Correctness Detecting of UML Activity Diagrams |
|
CHEN Huifeng,YU Xiaofei,JIANG Jianmin
|
( College of Mathematics and Informatics, Fujian Normal University, Fuzhou 350007, China)
|
| Abstract: UML activity diagrams are widely used in the software development process.But since they are semi-formal models,we can neither reason nor guarantee their correctness.In order to ensure their correctness,they must be transformed into formal models and then can be detected.Existing work has transformed activity diagrams into formal models such as transition systems,process algebras and Petri nets.However,these models need to add or decrease a large amount of information.In this paper,a new method is proposed,which directly transforms activity diagrams into formal models called dependency structures without adding or decreasing any information.Based on the dependency structure models,we first present a method of checking the correctness of a UML activity diagram and then introduce a corresponding tool.Finally,an example was used to demonstrate the checking process in detail.This work is helpful for software engineers to properly use UML activity diagram to analyze and design software systems. |
| Keywords: activity diagram;formal models;correctness |
