Generating Test Cases for Real-Time Systems Based on Symbolic Models

The state space explosion problem is one of the challenges to be faced by test case generation techniques, particularly when data values need to be enumerated. This problem gets even worse for real-time systems (RTS) that also have time constraints. The usual solution in this context, based on finite state machines or time automata, consists of enumerating data values (restricted to finite domains) while treating time symbolically. In this paper, a symbolic model for conformance testing of real-time systems software named TIOSTS that addresses both data and time symbolically is presented. Moreover, a test case generation process is defined to select more general test cases with variables and parameters that can be instantiated at testing execution time. Generation is based on a combination of symbolic execution and constraint solving for the data part and symbolic analysis for timed aspects. Furthermore, the practical application of the process is investigated through a case study.