The ever-increasing complexity of systems has motivated research in methodologies like model-based design (MBD) for managing and controlling the complexity of system development. MBD raises the level of abstraction of languages for specifying, designing, and implementing systems. MBD is supported by tools and techniques for automating steps in a development cycle.

Various forms of state machines have been proposed for specifying systems over the years, and there has been extensive research in algorithms to formally analyze state machines and automatically generate test cases to drive verification and validation processes.

This paper addresses a gap in the spectrum of research in test generation from state machines--and in particular input/output transition systems (IOTSs). IOTSs are asynchronous and help capture fine-grained interactions between I/O actions in a system. This is important as it may be difficult and even impossible to maintain a synchronous view of the system for verifying real-time and physical systems where the robustness of the system to the asynchronous nature of cause and effect is exactly what needs to be verified.

Early work in test generation [1] for IOTSs suffers from being stochastic in nature, and did not provide strong guarantees of finite and deterministic execution time for complete verification in the presence of uncontrolled asynchrony. However, imposing restrictions on asynchrony and considering Mealy IOTSs allows existing algorithms for synchronous finite-state machines to be used for test generation and to obtain completeness guarantees. A number of contemporary research efforts [2] address the same problem using slightly different hypotheses.

This area of research seems ripe for the systematization and rationalization of the different formalisms and algorithms to clarify tradeoffs and help practitioners select particular formalisms and algorithms for their applications.