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

摘要

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