| 基于时间自动机的UML模型转换与验证研究 |
| |
| 引用本文： | 姬莉霞,马建红.基于时间自动机的UML模型转换与验证研究[J].郑州大学学报(理学版),2013,45(1):50-55. |
| |
| 作者姓名： | 姬莉霞 马建红 |
| |
| 作者单位： | 郑州大学软件技术学院 河南郑州450002 |
| |
| 基金项目： | 河南省科技攻关计划项目,编号122102210518;河南省教育厅科学技术研究项目,编号12A520042 |
| |
| 摘 要： | 针对无法对UML模型进行形式化验证的问题,提出在元模型层将UML模型转换为时间自动机模型并进行验证的方法.形式化UML状态机的结构,抽象出UML和时间自动机的元模型,利用模型转换语言ATL对UML元模型和时间自动机元模型构造映射规则,实现UML模型到时间自动机模型的转换,在模型验证工具Uppaal中对转换结果进行形式化验证.最后进行实例研究,结果表明了此方法的有效性和先进性.
|
| 关 键 词： | 统一建模语言 模型验证 模型转换 Uppaal 时间自动机 元模型 |
Research on Model Transformation and Model Checking of UML Based on Timed Automata |
| |
| JI Li-xia
,
MA Jian-hong.Research on Model Transformation and Model Checking of UML Based on Timed Automata[J].Journal of Zhengzhou University:Natural Science Edition,2013,45(1):50-55. |
| |
| Authors: | JI Li-xia MA Jian-hong |
| |
| Institution: | (Software Technology School,Zhengzhou University,Zhengzhou 450002,China) |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
