Automated generation of test suites from formal specifications of real-time reactive systems

Real-time reactive systems are among the most difficult systems to test because of their size and complex time-dependent functionality. The number of test experiments for such systems is very large, if not infinite. Often such systems arise in safety-critical contexts. Hence, such systems require a rigorous analysis and thorough testing before they are deployed. This paper addresses test case generation methods and a metric-based test case selection algorithm for sufficient testing of real-time reactive systems. The methods are rigorous, and based on the formal specifications of the system and its fault models. The test generation and execution of algorithms are implemented in TROMLAB, a formal framework for developing real-time reactive systems. The methods are applied to the formal specification of the Train–Gate–Controller (TGC) example, a bench-mark case study in the real-time systems community. A brief description of the experimental results obtained on the case study is given.