Black-box conformance testing for real-time systems

We propose a new framework for black-box conformance testing of real-time systems, where specifications are modeled as non deterministic and partially-observable timed automata. We argue that such a model is essential for ease of modeling and expressiveness of specifications. The conformance relation is a timed extension of the input output conformance relation of [29]. We argue that it is better suited for testing than previously considered relations such as bisimulation, must/may preorder or trace inclusion. We propose algorithms to generate two types of tests for this setting: analog-clock tests which measure dense time precisely and digital-clock tests which measure time with a periodic clock. The latter are essential for implementability, since only finite-precision clocks are available in practice. We report on a prototype tool and a small case study. © Springer-Verlag 2004.