Generating Test Cases for Infinite System Specifications

Test case generation is a means to validate the implementation of a system <em>a posteriori</em> with respect to some given requirements imposed on the system. Current methods for the generation of test cases often rely on the system specification being given as a finite automaton, which does not fully cover the situation in systems with asynchronous communication, In this paper we present an algorithm for the computation of test cases for infinite system specifications.