Model Checking via Reachability Testing for Timed Automata
Luca Aceto November 1997 |
Abstract: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 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 of the ready simulation preorder, for nodes
of deterministic, Available as PostScript, PDF. |