| UPPAAL--一种适合自动验证实时系统的工具 |
| |
| 引用本文： | 郭华,庄雷,张习勇.UPPAAL--一种适合自动验证实时系统的工具[J].微计算机信息,2006,22(15):52-54. |
| |
| 作者姓名： | 郭华 庄雷 张习勇 |
| |
| 作者单位： | 1. 450052,郑州大学理论计算机研究所
2. 解放军信息工程大学 |
| |
| 基金项目： | 国家自然科学基金资助项目(69873040)河南省教育厅基础研究项目(2003520256) |
| |
| 摘 要： | UPPAAL是一个基于时间自动机的自动验证工具,已成功地用于实时控制器和通信协议等实时系统的验证.本文介绍了UPPAAL的语法,语义和语用,列举了它的几种扩展形式,并归纳了其应用及研究现状.
|
| 关 键 词： | UPPAAL 时间自动机 实时系统 模型检测 协议验证 |
| 文章编号： | 1008-0570(2006)05-3-0052-03 |
| 修稿时间： | 2005年9月14日 |
UPPAAL-a Tool Suit for Automatic Verification of Real-time Systems |
| |
| Guo Hua,Zhuang Lei,Zhang Xiyong.UPPAAL-a Tool Suit for Automatic Verification of Real-time Systems[J].Control & Automation,2006,22(15):52-54. |
| |
| Authors: | Guo Hua Zhuang Lei Zhang Xiyong |
| |
| Abstract: | UPPAAL is a tool suit for automatic verification based on timed automata, which has been used to verify real-time controllers andcommunication protocols successfully. This paper outlines the syntax, semantics and pragmatics of UPPAAL, and reports on newdirectionsthat extends UPPAAL with several modeling. At last we describe a selection of the case studies, and sum up the relevant work. |
| |
| Keywords: | UPPAAL timed automata real-time system model checking protocol verification |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
