摘要
在传统的UML Statechart图中加入了数据流对象后,因为UML Statechart图缺乏精确的数据流语义,所以不适合应用UML Statechart图对工作流中的数据流进行建模并验证其正确性。为了解决这一问题,选择标记转换系统(LTS)作为语义域,并用结构化操作语义(SOS)分两步定义了UML Statechart图的数据流语义,为工作流中的数据流正确性验证奠定了基础。在此基础上,使用时序逻辑公式表示数据流所需满足的性质,在验证数据流的正确性之前,给出了将它的UML Statechart图模型转化为可达状态迁移图的算法,最后通过模型检测算法验证数据流的正确性。
After being integrated with data flow objects,traditional UML Statecharts are not suited for modeling and the verification of the data flow in the workflows due to the lack of the exact semantics of the data flow.To solve the problem,LTS is selected 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.Based on this,temporal logic formula is used to express the properties that the data flow must satisfy,before the verification,an algorithm transforming the UML Statecharts model into reachable state transition graph is given ,finally the correctness of the data flow is verified by model checking technique.
出处
《计算机工程与应用》
CSCD
北大核心
2009年第24期56-59,共4页
Computer Engineering and Applications
基金
国家自然科学基金No60073020
江苏省高校自然科学研究项目No05KJB520119~~
