A consistency-based approach to efficient test case generation from timed automata specifications

In this paper we describe the PROPeRTy project (Propagation Rules for Real-Time Systems) ongoing at the University of Erlangen-Nuremberg, a framework for testing real-time systems using logic programming approach combined with consistency techniques. A realtime system specification relies on the timed automata model [R. Alur et al. (1994)] and is automatically executed allowing the user to study the behaviour of the system by specifying constraints under which the execution should be performed. Such constraints, taken into account during a symbolic execution, are resolved by constraint propagator under consistency preserving. The symbolic execution generates a path (or multiple paths) consistent with the user formula and helps to decide if the formula is satisfied by the specification. In this paper we report about our project on using constraint propagation in the testing such realtime systems.