UML模型检测方法的研究

• 作者: 张频 罗贵明
• 来源期刊: 计算机应用
• 学科: 工学
• 关键词: 模型检测 统一建模语言 层次自动机 简单进程元语言解释器 PROMELA
• 年，卷（期）: 2007,（10）
• 所属期刊栏目: 人工智能与软件过程技术
• 页码范围: 2493-2497,2500
• 页数: 6页
• 分类号: TP311.5
• 字数: 7008字
• 语种: 中文

摘要

统一建模语言(UML)是设计和分析软件系统最常用的方法,如何保证UML模型满足某些特性是一个非常重要的问题,而模型检测是一种能够有效提高系统可靠性的自动化技术.研究了使用简单进程元语言解释器(SPIN)对UML模型进行检测的方法.首先对UML模型进行形式化描述,使用层次自动机来描述状态图,然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA,使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束,通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题.项目组基于此方法还开发了一套模型检测工具UMLChecker.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗贵明	清华大学软件学院	19	125	6.0	10.0
2	张频	清华大学软件学院	1	29	1.0	1.0