Digitisation and full abstraction for dense-time model checking

Abstract

We study the digitisation of dense-time behaviours of timed processes, and show how this leads to exact verification methods for a large class of dense-time specifications. These specifications are all closed under inverse digitisation, a robustness property first introduced by Hen-zinger, Manna, and Pnueli (on timed traces), and extended here to timed failures, enabling us to consider liveness issues in addition to safety properties. We discuss a corresponding model checking algorithm and show that, in many cases, automated verification of such dense-time specifications can in fact be directly performed on the model checker FDR (a commercial product of Formal Systems (Europe) Ltd.). We illustrate this with a small case study (the railway level crossing problem). Finally, we show that integral-or digitised-behaviours are fully abstract with respect to specifications closed under inverse digitisation, and relate this to the efficiency of our model checking algorithm. © Springer-Verlag Berlin Heidelberg 2002.