首页 | 本学科首页   官方微博 | 高级检索  
     

基于UPPAAL的实时系统模型验证
引用本文:周清雷,姬莉霞,王艳梅.基于UPPAAL的实时系统模型验证[J].计算机应用,2004,24(9):129-131.
作者姓名:周清雷  姬莉霞  王艳梅
作者单位:1. 郑州大学,信息工程学院,河南,郑州,450052;信息工程大学,信息工程学院,河南,郑州,450002
2. 郑州大学,信息工程学院,河南,郑州,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 维普 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号