Since 2014
Model Checking via Reachability Testing for Timed Automata
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Model Checking via Reachability Testing for Timed Automata
|
|
| Creator |
Aceto, Luca
Burgueno, Augusto Larsen, Kim G. |
|
| Description |
In this paper we develop an approach to model-checking for timed automata via reachability testing. As our specification formalism, we consider a dense-time logic with clocks. This logic may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every logical formula phi, a so-called test automaton T_phi in such a way that checking whether a system S satisfies the property phi can be reduced to a reachability question over the system obtained by making T_phi interact with S. The testable logic we consider is both of practical and theoretical interest. On the practical side, we have used the logic, and the associated approach to model-checking via reachability testing it supports, in the specification and verification in Uppaal of a collision avoidance protocol. On the theoretical side, we show that the logic is powerful enough to permit the definition of characteristic properties, with respect to a timed version ofthe ready simulation preorder, for nodes of deterministic, tau-free timed automata. This allows one to compute behavioural relations via our model-checking technique, therefore effectively reducing the problem of checking the existence of a behavioural relation among states of a timed automaton to a reachability problem.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1997-01-29
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18955
10.7146/brics.v4i29.18955 |
|
| Source |
BRICS Report Series; No 29 (1997): RS-29 Model Checking via Reachability Testing for Timed Automata
BRICS Report Series; Nr. 29 (1997): RS-29 Model Checking via Reachability Testing for Timed Automata 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18955/16594
|
|