基于UPPAAL的实时系统模型验证

被引：23

作者：

周清雷

姬莉霞

王艳梅

机构：

[1] 郑州大学信息工程学院

[2] 郑州大学信息工程学院河南郑州信息工程大学信息工程学院

[3] 河南郑州

来源：

计算机应用 | 2004年 / 09期

关键词：

实时系统; 模型检查; 时间自动机; UPPAAL;

D O I：

暂无

中图分类号：

TP316.2 [实时操作系统]; TP301.1 [自动机理论];

学科分类号：

081202 ; 0835 ;

摘要：

UPPAAL是一种使用时间自动机模型的实时系统验证工具 ,它可以避免时间自动机求积时状态空间的爆炸。介绍了时间自动机理论和工具UPPAAL ,着重说明如何用UPPAAL进行模型检查 ,并给出了一个应用实例

引用

页码：129 / 131

页数：3

共 7 条

[1]

An Integrated Aproach to Modeling and Analysis of Embedded Real-Time Systems Based on Timed Petri Nets. Gu Z,Shin KG. Proceeding of 23rd International Conference on Disributed Computing Systems (ICDCS 03 ) . 2003

[2]

Hierarchical Timed Automata for UPPAAL. David A,Yi W. 10th Nordic Workshop on Programming Theory (NWPT 98 ) . 1998

[3]

NATO-AST1998 Summer School on Veri-fication of Digital and Hybrid Systems. Alur R,Timed Automata. . 1998

[4]

A theory of timed automata. Alur R,Dill,DL. Theoretical Computer Science . 1994

[5]

Automata for Modeling Real-Time Systems. Alur R,Dill DL. Proc 17th International Colloquium on Automata, Languages and Programming, 443 of Lecture Notes in Computer Science[C] . 1990

[6]

Models for reactivity. Manna Z,Pnueli A. Acta Informatica . 1993

[7]

UPPAAL-aToolforAutomaticVerificationofReal timeSystems. BengtssonJ,LarssonF,LarsonF,etal. ProceedingsofWorkshoponVerificationandControlofHybridSystemsIII . 1995

← 1 →