定义及验证UML Statechart图中的数据流语义

作者：陆公正; 吴澜波; 张广泉

来源：计算机工程与应用, 2009, (24): 56-59.

• 统一建模语言(UML)
• UML Statechart图
• 数据流语义
• 时序逻辑
• 验证
• 模型检测 Unified Modeling Language(UML)
• UML Statecharts
• semantics of data flow
• temporal logic
• verification
• model checking

在传统的UML Statechart图中加入了数据流对象后,因为UML Statechart图缺乏精确的数据流语义,所以不适合应用UML Statechart图对工作流中的数据流进行建模并验证其正确性。为了解决这一问题,选择标记转换系统(LTS)作为语义域,并用结构化操作语义(SOS)分两步定义了UML Statechart图的数据流语义,为工作流中的数据流正确性验证奠定了基础。在此基础上,使用时序逻辑公式表示数据流所需满足的性质,在验证数据流的正确性之前,给出了将它的UML Statechart图模型转化为可达状态迁移图的算法,最后通过模型检测算法验证数据流的正确性。

• 出版日期2009
• 单位苏州市职业大学; 苏州大学; 苏州卫生职业技术学院