| 基于UPPAAL的实时系统模型验证 |
| |
| 引用本文： | 周清雷,姬莉霞,王艳梅. 基于UPPAAL的实时系统模型验证[J]. 计算机应用, 2004, 24(9): 129-131 |
| |
| 作者姓名： | 周清雷 姬莉霞 王艳梅 |
| |
| 作者单位： | 郑州大学,信息工程学院,河南,郑州,450052;信息工程大学,信息工程学院,河南,郑州,450002;郑州大学,信息工程学院,河南,郑州,450052 |
| |
| 摘 要： | UPPAAL是一种使用时间自动机模型的实时系统验证工具，它可以避免时间自动机求积时状态空间的爆炸。介绍了时间自动机理论和工具UPPAAL，着重说明如何用UPPAAL进行模型检查，并给出了一个应用实例。
|
| 关 键 词： | 实时系统 模型检查 时间自动机 UPPAAL |
| 文章编号： | 1001-9081(2004)09-0129-03 |
Model checking of real-time systems based on UPPAAL |
| |
| ZHOU Qing-lei. Model checking of real-time systems based on UPPAAL[J]. Journal of Computer Applications, 2004, 24(9): 129-131 |
| |
| Authors: | ZHOU Qing-lei |
| |
| Affiliation: | ZHOU Qing-lei~ |
| |
| Abstract: | UPPAAL is a tool for real-time system verification using timed automata model. UPPAAL can avoid the state space explosion when computing the product of timed automata. We introduced the theory of timed automata and UPPAAL, described how UPPAAL worked and gave an example of its application. Last, the development and foreground of UPPAAL were discussed. |
| |
| Keywords: | real-time systems model checking timed automata UPPAAL |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
