%0 Journal Article
%T 一种UML状态图模型检测方法
%A 张涛
%A 黄少滨
%A 黄宏涛
%A 吕天阳
%A 刘刚
%J 哈尔滨工程大学学报
%D 2011
%R doi:10.3969/j.issn.1006-7043.2011.08.013
%X 为在开发过程早期发现系统设计的各种错误与不一致，提出一种UML状态图模型检测方法，用于验证设计模型与需求规约间的一致性.该方法通过元组定义UML状态图的主要元素，给出状态图的中间表示形式SC.基于SC上定义的操作语义，该方法将状态图转换为具有KRIPKE语义结构的状态迁移系统，并将系统需满足的性质表示为线性时序逻辑公式，用模型检测技术验证状态迁移系统对线性时序逻辑公式的满足性.该方法可以转换更多的状态图元素，缩减状态图迁移系统的状态空间及提高模型检测效率.
%K 模型检测
%K 迁移系统
%K 操作语义
%K UML
%K 状态图
%U http://heuxb.hrbeu.edu.cn/oa/darticle.aspx?type=view&id=20110813