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

Real-time reactive systems are among the most difficult systems to design and implement because of their size and complex functional and timing requirements. They are often used in safety-critical contexts. Consequently, the correction of such systems must be assured before they are deployed. This thesis addresses the quality assurance of real-time reactive systems through rigorous testing methods. The thesis gives methods to generate test cases from the formal specifications of real-time reactive systems developed in TROMLAB framework. The scope of this thesis encompasses two major components. A Homomorphism Theorem is given that serves as a basis for automated test case generation from the grid automaton associated with the extended state machine formalism. A number of algorithms are also given for generating test cases for black-box testing of reactive class implementations, implementations of class refinements and system configurations. The testing methodologies are theoretically sound, yet being practical for automated test case generation.