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

doi:10.3778/j.issn.1002-8331.2009.24.018

计算机工程与应用 ›› 2009, Vol. 45 ›› Issue (24): 56-59.DOI: 10.3778/j.issn.1002-8331.2009.24.018

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

陆公正¹，吴澜波₂，张广泉³

1.苏州市职业大学计算机工程系，江苏苏州 215104
2.苏州卫生职业技术学院检验药学系，江苏苏州 215009
3.苏州大学计算机科学与技术学院，江苏苏州 215006

收稿日期:2008-05-08 修回日期:2008-08-31 出版日期:2009-08-21 发布日期:2009-08-21
通讯作者: 陆公正

Definition and verification of semantics of data flow in UML Statecharts

LU Gong-zheng¹，WU Lan-bo²，ZHANG Guang-quan³

1.Department of Computer Engineering，Suzhou Vocational University，Suzhou，Jiangsu 215104，China
2.Department of LAB TEC and Pharmacy，Suzhou Health College，Suzhou，Jiangsu 215009，China
3.School of Computer Science and Technology，Soochow University，Suzhou，Jiangsu 215006，China

Received:2008-05-08 Revised:2008-08-31 Online:2009-08-21 Published:2009-08-21
Contact: LU Gong-zheng

摘要/Abstract

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

关键词: 统一建模语言（UML）, UML Statechart图, 数据流语义, 时序逻辑, 验证, 模型检测

Abstract: 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.

Key words: Unified Modeling Language（UML）, UML Statecharts, semantics of data flow, temporal logic, verification, model checking

中图分类号:

TP311

陆公正¹，吴澜波₂，张广泉³. 定义及验证UML Statechart图中的数据流语义[J]. 计算机工程与应用, 2009, 45(24): 56-59.

LU Gong-zheng¹，WU Lan-bo²，ZHANG Guang-quan³. Definition and verification of semantics of data flow in UML Statecharts[J]. Computer Engineering and Applications, 2009, 45(24): 56-59.

[1]	郑亮，陈亚，陈小潘，郑逢斌. 人脸局部特征增强的亲属关系验证方法[J]. 计算机工程与应用, 2021, 57(23): 226-233.
[2]	李舵，董超群，司品超，何曼，刘钱超. 神经网络验证和测试技术研究综述[J]. 计算机工程与应用, 2021, 57(22): 53-67.
[3]	王洁，金正猛，冯灿. 自适应广义全变差的图像泊松去噪算法[J]. 计算机工程与应用, 2021, 57(20): 203-209.
[4]	舒乐，戴佳筑. 基于通用对抗扰动的图像验证码保护方法[J]. 计算机工程与应用, 2021, 57(18): 135-141.
[5]	谭莉娟，郑巍，刘友林，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证方法综述[J]. 计算机工程与应用, 2021, 57(15): 9-22.
[6]	刘友林，郑巍，谭莉娟，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证工具综述[J]. 计算机工程与应用, 2021, 57(11): 1-10.
[7]	吴杰，段锦，董锁芹，李英超. DFM-GAN网络在跨年龄模拟的人脸识别技术研究[J]. 计算机工程与应用, 2021, 57(10): 117-124.
[8]	谢艺菲，卢琪，刘鑫，胡亚豪，潘志松，陈浩. 基于图的多层次注意力事实验证算法[J]. 计算机工程与应用, 2021, 57(10): 146-153.
[9]	仝乐，郝蓉，于佳. 单服务器上的双线性配对安全外包方案[J]. 计算机工程与应用, 2020, 56(9): 131-135.
[10]	曹廷荣，陆玲，龚燕红，贾惠珍. 基于对抗网络的验证码识别方法[J]. 计算机工程与应用, 2020, 56(8): 199-204.
[11]	姜娇，蔡林沁，韦鹏程，李莉. 支持可验证的密文模糊关键字检索方案[J]. 计算机工程与应用, 2020, 56(7): 74-80.
[12]	王夫森，李志淮，田娜. 提升分片规模和有效性的多轮PBFT验证方案[J]. 计算机工程与应用, 2020, 56(24): 102-108.
[13]	陈虹，朱亚囡，肖成龙，金海波，张子浩. 可公开验证无证书的多接收者匿名签密方案[J]. 计算机工程与应用, 2020, 56(19): 120-125.
[14]	厍向阳，刘巧，叶鸥. 融合LeNet-5和Siamese神经网络模型的人脸认证算法研究[J]. 计算机工程与应用, 2020, 56(15): 215-220.
[15]	刘丽伟1，孙践知1，谭励1，杨斌2. 关于IMC/IMV的网络设备可信认证方法研究[J]. 计算机工程与应用, 2019, 55(9): 79-86.

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

Definition and verification of semantics of data flow in UML Statecharts

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics