Testing Real-Time Constraints in a Process Algebraic Setting

Verifying timing properties of real-time systems by traditional approaches that depend on the exploration of the entire system state space is impractical for large systems. In contrast, 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. We present a domain testing based technique for verifying timing constraints of real-time systems, given timing constraints specified as minimum and maximum allowable delays between input/output events. The testing methodology is presented in a process algebraic setting where it is an efficient alternative to model checking for verifying system timing properties. An example illustrates the application of our testing technique to a timed interactive system.