UML Statecharts的模型检验方法

• 作者: 王戟 董威 齐治昌
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: UML(unified modeling language) Statecharts 模型检验 ω自动机
• 年，卷（期）: 2003,（4）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 750-756
• 页数: 7页
• 分类号: TP311
• 字数: 6598字
• 语种: 中文

摘要

统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Büchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王戟	国防科学技术大学计算机学院	44	1257	17.0	35.0
2	董威	国防科学技术大学计算机学院	32	402	10.0	19.0
3	齐治昌	国防科学技术大学计算机学院	38	881	15.0	29.0