UPPAAL — a tool suite for automatic verification of real-time systems

1996 ◽  
pp. 232-243 ◽  
Author(s):  
Johan Bengtsson ◽  
Kim Larsen ◽  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Real Time ◽  
Automatic Verification ◽  
Real Time Systems ◽  
Time Systems

scholarly journals UPPAAL in 1995

1996 ◽  
Vol 3 (60) ◽  
Author(s):  
Johan Bengtsson ◽  
Kim G. Larsen ◽  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Real Time ◽  
Case Studies ◽  
Theoretical Foundation ◽  
Timed Automata ◽  
Automatic Verification ◽  
Real Time Systems ◽  
The Past ◽  
Liveness Properties ◽  
Time Systems

UPPAAL is a tool suite for automatic verification of safety and<br />bounded liveness properties of real-time systems modeled as networks of timed automata<br />[12, 9, 4], developed during the past two years. In this paper, we summarize<br />the main features of UPPAAL in particular its various extensions developed in 1995<br />as well as applications to various case-studies, review and provide pointers to the<br />theoretical foundation.

scholarly journals Diagnostic Model Checking for Real-Time Systems

1996 ◽  
Vol 3 (57) ◽  
Author(s):  
Kim G. Larsen ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Automatic Verification ◽  
Diagnostic Feature ◽  
Diagnostic Model ◽  
Graphical Interface ◽  
Real Time Systems ◽  
Control Protocol ◽  
Time Systems

Uppaal is a new tool suit for automatic verification of networks of<br />timed automata. In this paper we describe the diagnostic model-checking feature<br />of Uppaal and illustrates its usefulness through the debugging of (a version<br />of) the Philips Audio-Control Protocol. Together with a graphical interface of<br />Uppaal this diagnostic feature allows for a number of errors to be more easily<br />detected and corrected.

scholarly journals Compositional and Symbolic Model-Checking of Real-Time Systems

1996 ◽  
Vol 3 (59) ◽  
Author(s):  
Kim G. Larsen ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Symbolic Model Checking ◽  
Automatic Verification ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Symbolic Model ◽  
Verification Tools ◽  
State Region ◽  
Time Systems

Efficient automatic model-checking algorithms for<br />real-time systems have been obtained in recent years<br />based on the state-region graph technique of Alur,<br />Courcoubetis and Dill. However, these algorithms are<br />faced with two potential types of explosion arising from<br />parallel composition: explosion in the space of control<br />nodes, and explosion in the region space over clock variables.<br />In this paper we attack these explosion problems by<br />developing and combining compositional and symbolic<br />model-checking techniques. The presented techniques<br />provide the foundation for a new automatic verification<br />tool Uppaal. Experimental results indicate that<br />Uppaal performs time- and space-wise favorably compared<br />with other real-time verification tools.

scholarly journals UPPAAL—a Tool Suite for Automatic Verification of Real–Time Systems

1996 ◽  
Vol 3 (58) ◽  
Author(s):  
Johan Bengtsson ◽  
Kim G. Larsen ◽  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
Automatic Verification ◽  
Graphical Interface ◽  
Real Time Systems ◽  
Model Checker ◽  
Current Version ◽  
Textual Representations ◽  
Liveness Properties ◽  
Time Systems

Uppaal is a tool suite for automatic verification of safety and<br />bounded liveness properties of real-time systems modeled as networks of<br />timed automata. It includes: a graphical interface that supports graphical<br />and textual representations of networks of timed automata, and automatic<br />transformation from graphical representations to textual format,<br />a compiler that transforms a certain class of linear hybrid systems to<br />networks of timed automata, and a model-checker which is implemented<br />based on constraint-solving techniques. Uppaal also supports diagnostic<br />model-checking providing diagnostic information in case verification of a<br />particular real-time systems fails.<br />The current version of Uppaal is available on the World Wide Web via<br />the Uppaal home page http://www.docs.uu.se/docs/rtmv/uppaal.

scholarly journals Synthesizing Distinguishing Formulae for Real Time Systems

1994 ◽  
Vol 1 (48) ◽  
Author(s):  
Jens Chr. Godskesen
Keyword(s):  
Real Time ◽  
Diagnostic Information ◽  
Automatic Verification ◽  
Real Time Systems ◽  
Logical Formula ◽  
Verification Tool ◽  
Parallel Networks ◽  
Bisimulation Equivalence ◽  
Time Systems

This paper describes a technique for generating diagnostic information for the <em>timed</em> bisimulation equivalence and the <em>timed</em> simulation preorder. More precisely, given two (parallel) networks of regular real-time processes, the technique will provide a logical formula that differentiates them in case they are not timed (bi)similar. Our method may be seen as an extension of the algorithm by Cerans for deciding timed bisimilarity in that information of time-quantities has been added sufficient for generating distinguishing formulae. The technique has been added to the automatic verification tool E<small>PSILON</small> and applied to various examples.

Sign in / Sign up

Export Citation Format

Share Document