Testing real-time constraints

The verification of timing properties of real-time system models by traditional approaches that depend on the exploration of the entire system state space is impractical for large systems. In constrast, testing allows the search for violations of a property to be narrowed to a relatively small portion of the overall state space, based on assumptions regarding the structure of an implementation. In a computer systems engineering context the primary advantages of testing over traditional state-space exploration approaches are two-fold. First, testing offers the possibility of model validation without state space explosion. Second, the tests themselves are produced as an artifact of model validation. Thus, the same tests that validated the model can be used to validate the hardware or software implementation that is created from it. We present a framework for testing timing constraints of real-time systems. These tests are based on specifications of minimum and maximum allowable delays between input/output events in the execution of a system. We present specification and test languages and their formal semantics, and formalize a new hierarchy of test coverage criteria for domain testing of real-time properties. Based on these test coverage criteria, techniques for automatically deriving optimized test suites are presented. Our testing framework and optimization techniques are illustrated with examples and a substantial case study