基于TLA的UML模型形式化验证

• 作者: 李刚 梁盟磊 王小平 薛小平
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 形式化方法 形式化验证 统一建模语言 行为时序逻辑
• 年，卷（期）: 2011,（2）
• 页码范围: 72-74
• 分类号: TP391
• 字数: 3320字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2011.02.025

摘要

统一建模语言(UML)不能直接对所建直模型的正确性进行形式化验证.为解决上述问题,从UML模型的静态结构和动态行为2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性.通过实例分析证明了该方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李刚	同济大学电子与信息工程学院信息与通信工程系	96	924	16.0	28.0
2	王小平	同济大学电子与信息工程学院计算机科学与技术系	109	940	18.0	24.0
3	薛小平	同济大学电子与信息工程学院信息与通信工程系	54	511	13.0	21.0
4	梁盟磊	同济大学电子与信息工程学院计算机科学与技术系	2	14	2.0	2.0