Conformance testing is a promising approach to system verification and validation, because test cases can be automatically generated. In such cases, specification and implementation are associated by a conformance relation so that the results of test case execution can be precisely interpreted. However, these test case generation techniques face important challenges, such as state space explosion. Such problems are even worse when time constraints come into play, for example, in real-time systems (RTS). Typical solutions are based on model checking, finite-state machines (FSMs), and time automata, and involve enumerating data values (only for finite-domain scenarios) and treating time symbolically. It is worth noting that enumerating all possible values in a model is not usually needed for testing, since only a very few combinations can be considered. The authors of this paper propose TIOSTS, a symbolic model for conformance testing of RTS that handles both data and time by extending timed automata and input/output (I/O) symbolic transitions systems. Symbolic execution is a well-known technique that handles the state space explosion problem by analyzing programs based on symbolic rather than concrete values.

Test case generation involves deriving test cases from specifications (that is, a formal model of the system under test (SUT) presented in the TIOSTS format) to check the conformance between specifications and implementations. The proposed approach focuses on the use of manual activity, where the tester indicates the scenarios for which the test cases will be generated. Using specific operations, test cases are selected from the symbolic execution tree generated by the process. To comply with RTS programs, generated test cases can be interruptible. The authors prove that for every specification, all test suites generated by the approach are sound.

The paper ends with a case study designed to generate and execute test cases for an alarm system, where the approach is supplemented by SYMBOLRT, a helper tool. The results are interesting, compared to other techniques that suffer from state space explosion. The authors intend to assess their approach with embedded systems in future work.