Moez Krichen and Stavros Tripakis
An Expressive and Implementable Formal Framework for Testing Real-Time Systems (2004)
An Expressive and Implementable Formal Framework for Testing Real-Time Systems (2004)
TR-2004-13.pdf
Keywords: real-time systems, timed automata, conformance testing, black-box, partial observability, coverage
Abstract: We propose a new framework for black-box conformance testing of real-time systems. The framework is based on the model of partially-observable, non-deterministic timed automata. We argue that partial observability and non-determinism are essential features for ease of modeling, expressiveness and implementability. We provide algorithms for on-the-fly or static generation of digital-clock tests. These tests measure time only with finite-precision, periodic clocks, another essential condition for implementability. We also propose a technique for location and edge coverage of the specification, by reducing the problem to covering a symbolic reachability graph. We report on a prototype tool and two case studies.
