Development and evaluation of symbolic model checker based on approximation for real-time systems

2004 ◽  
Vol 35 (10) ◽  
pp. 83-101 ◽  
Author(s):  
Satoshi Yamane ◽  
Kazuhiro Nakamura
Keyword(s):  
Real Time ◽  
Real Time Systems ◽  
Model Checker ◽  
Symbolic Model ◽  
Time Systems

scholarly journals Symbolic Model Checking for Real-Time Systems

1994 ◽  
Vol 111 (2) ◽  
pp. 193-244 ◽  
Author(s):  
T.A. Henzinger ◽  
X. Nicollin ◽  
J. Sifakis ◽  
S. Yovine
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Symbolic Model Checking ◽  
Real Time Systems ◽  
Symbolic Model ◽  
Time Systems

scholarly journals Online On-the-Fly Testing of Real-time Systems

2003 ◽  
Vol 10 (49) ◽  
Author(s):  
Marius Mikucionis ◽  
Kim G. Larsen ◽  
Brian Nielsen
Keyword(s):  
Real Time ◽  
Test Generation ◽  
Timed Automata ◽  
Online Testing ◽  
Real Time Systems ◽  
Model Checker ◽  
Test Specification ◽  
And Performance ◽  
Automata Network ◽  
Time Systems

In this paper we present a framework, an algorithm and a new tool for online testing of real-time systems based on symbolic techniques used in UPPAAL model checker. We extend UPPAAL timed automata network model to a test specification which is used to generate test primitives and to check the correctness of system responses including the timing aspects. We use timed trace inclusion as a conformance relation between system and specification to draw a test verdict. The test generation and execution algorithm is implemented as an extension to UPPAAL and experiments carried out to examine the correctness and performance of the tool. The experiment results are promising.

Symbolic model checking for discrete real-time systems

2017 ◽  
Vol 61 (5) ◽  
Author(s):  
Xiangyu Luo ◽  
Lijun Wu ◽  
Qingliang Chen ◽  
Haibo Li ◽  
Lixiao Zheng ◽  
...  
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Symbolic Model Checking ◽  
Real Time Systems ◽  
Symbolic Model ◽  
Time Systems

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.

Sign in / Sign up

Export Citation Format

Share Document