Specification and Test of Real-Time Systems

Distributed real-time computer based systems are very complex and intrinsically difficult to specify and implement correctly; in part this is caused by the overwhelming number of possible interactions between system components, but especially by a lack of adequate methods and tools to deal with this complexity. This thesis proposes new specification and testing techniques. We propose a real-time specification language which facilitates modular specification and programming of reusable components. A specification consists of a set of concurrent untimed components which describes the functional behavior of the system, and a set of constraint patterns which describes and enforces the timing and synchronization constraints among components. We propose new techniques for automated black box conformance testing of real-time systems against densely timed speci cations. A test generator tool examines a specification of the desired system behavior and generates the necessary test cases. A main problem is to construct a reasonably small test suite that can be executed within allotted resources, while having a high likelihood of detecting unknown errors. Our goal has been to treat the time dimension of this problem thoroughly. Based on a determinizable class of timed automata, Event Recording Automata, we show how to systematically and automatically generate tests in accordance with Hennessy's classical testing theory lifted to include timed traces. We select test cases from a coarse grained state space partitioning of the specification, and cover each partition with at least one test case, possibly selecting extreme clock values. In a partition, the system behavior remains the same independently of the actual clock values. We employ the efficient symbolic constraint solving techniques originally developed for model checking of real-time systems to compute the reachable parts of these equivalence classes, to synthesize the timed tests, and to guarantee a coverage of the equivalence class partitioning. We have implemented our techniques in the RTCAT test case generation tool. Through a series of examples we demonstrate how Event Recording Automata can specify untrivial and practically relevant timing behavior. Despite being theoretically less expressive than timed automata, it has proven sufficiently expressive for our examples, but sometimes causing minor inconveniences. Applying RTCAT to generate tests from these speciffications, including the Philips Audio Protocol, resulted in encouragingly small test suites. We conclude that our approach is feasible and deserves further work, but also that it should be generalized and allow timing uncertainty and modeling of the environment. Some implementation improvements are also necessary.