| 基于TLA的UML模型形式化验证 |
| |
| 引用本文： | 梁盟磊,王小平,薛小平,李刚.基于TLA的UML模型形式化验证[J].计算机工程,2011,37(2):72-74. |
| |
| 作者姓名： | 梁盟磊 王小平 薛小平 李刚 |
| |
| 作者单位： | 1. 同济大学电子与信息工程学院计算机科学与技术系,上海,200092
2. 同济大学电子与信息工程学院信息与通信工程系,上海,200092 |
| |
| 基金项目： | 国家自然科学基金资助项目(60972036) |
| |
| 摘 要： | 统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题，从UML模型的静态结构和动态行为 2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法，在此基础上提出将UML模型转化为TLA+的形式化描述方法，并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。
|
| 关 键 词： | 形式化方法 形式化验证 统一建模语言 行为时序逻辑 |
Formal Verification of UML Models Based on TLA |
| |
| LIANG Meng-lei,WANG Xiao-ping,XUE Xiao-ping,LI Gang.Formal Verification of UML Models Based on TLA[J].Computer Engineering,2011,37(2):72-74. |
| |
| Authors: | LIANG Meng-lei WANG Xiao-ping XUE Xiao-ping LI Gang |
| |
| Affiliation: | LIANG Meng-leia,WANG Xiao-pinga,XUE Xiao-pingb,LI Gangb(a.Department of Computer Science and Technology,b.Department of Information and Communication Engineering,College of Electronics and Information,Tongji University,Shanghai 200092,China) |
| |
| Abstract: | |
| |
| Keywords: | formal method formal verification UML Temporal Logic of Actions(TLA) |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
|
