中文摘要：

由于UML Statechart图缺乏精确的数据流语义，因而难以对UML Statechart图建模的工作流的数据流进行正确性验证．首先，UML Statechart图是基于状态转换的，为此选择标记转换系统（LTS）作为语义域，并用结构化操作语义（sos）分两步定义了UML Statechart图的数据流语义．然后，采用时序逻辑公式表示数据流所需满足的性质，同时给出了将UML Statechart图模型转化为可达状态迁移图的算法，最后通过模型检测算法验证数据流的正确性．

英文摘要：

Due to traditional UML Statecharts lack of exact semantics of data flow, the verification of the data flow in the workflows modeled by it is very hard to perform. To solve this issue, LTS is first selected in this paper as the semantic field, and the semantics of data flow are defined with SOS in two steps so as to lay the foundation for the verification of the data flow of the Workflow. Then, temporal logic formula is used to express the property requirements the data flow must meet before the verification, an algorithm transforming the UML Statecharts model into reachable state transition graph is presented. Finally the correctness of the data flow is verified by model checking technique.