Automatic verification of fault tolerance using model checking

2002 ◽  
Author(s):  
T. Yokogawa ◽  
T. Tsuchiya ◽  
T. Kikuno
Keyword(s):  
Fault Tolerance ◽  
Model Checking ◽  
Automatic Verification

scholarly journals From Timed Automata to Logic - and Back

1995 ◽  
Vol 2 (2) ◽  
Author(s):  
Francois Laroussinie ◽  
Kim G. Larsen ◽  
Carsten Weise
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Finite Automata ◽  
Automatic Verification ◽  
Satisfiability Problem ◽  
Timed Automaton

One of the most successful techniques for automatic verification is that<br />of model checking. For finite automata there exist since long extremely<br />efficient model-checking algorithms, and in the last few years these algorithms have been made applicable to the verification of real-time automata using the region-techniques of Alur and Dill.<br />In this paper, we continue this transfer of existing techniques from the<br />setting of finite (untimed) automata to that of timed automata. In particular, a timed logic L is put forward, which is sufficiently expressive that we for any timed automaton may construct a single characteristic L formula uniquely characterizing the automaton up to timed bisimilarity. Also, we prove decidability of the satisfiability problem for L with respect to given bounds on the number of clocks and constants of the timed automata to be constructed. None of these results have as yet been succesfully accounted for in the presence of time.

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 On Construction and Verification of PLC-Programs

2015 ◽  
Vol 19 (4) ◽  
pp. 25-36 ◽  
Author(s):  
E. V. Kuzmin ◽  
V. A. Sokolov
Keyword(s):  
Model Checking ◽  
Automatic Verification ◽  
Programmable Logic ◽  
Programmable Logic Controllers ◽  
Program Correctness ◽  
Verification Tool ◽  
Discrete Problems ◽  
Plc Program ◽  
Logic Controllers

We review some methods and approaches to programming discrete problems for Programmable Logic Controllers on the example of constructing PLC-programs for controling a code lock. For these approaches we evaluate the usability of the model checking method for the analysis of program correctness with respect to the automatic verification tool Cadence SMV. Some possible PLC-program vulnerabilities arising at a number approaches to programming of PLC are revealed.

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