UML Statechart图中数据流的语义及验证
陆公正1
吴澜波2
于复生1
张广泉3
1.苏州市职业大学,计算机工程系,江苏,苏州,2151042.苏州卫生职业技术学院,检验药学系,江苏,苏州,2150093.苏州大学,计算机科学与技术学院,江苏,苏州,215006
摘要：由于UML Statechart图缺乏精确的数据流语义,因而难以对UML Statechart图建模的工作流的数据流进行正确性验证.首先,UML Statechart图是基于状态转换的,为此选择标记转换系统(LTS)作为语义域,并用结构化操作语义(SOS)分两步定义了UML Statechart图的数据流语义.然后,采用时序逻辑公式表示数据流所需满足的性质,同时给出了将UML Statechart图模型转化为可达状态迁移图的算法,最后通过模型检测算法验证数据流的正确性.
关键词：UML Statechart图数据流语义时序逻辑验证模型检测
分类号：TP311(计算技术、计算机技术)
资助基金：国家自然科学基金(60073020)江苏省高等学校自然科学研究项目(05KJB520119)
论文发表日期：2009-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：6( 60-65 )
英文信息