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

• Main Author: Zheng, Mao
• Format: Others
• Published: 2002
• Online Access: http://spectrum.library.concordia.ca/1575/1/NQ68212.pdf; Zheng, Mao <http://spectrum.library.concordia.ca/view/creators/Zheng=3AMao=3A=3A.html> (2002) Automated test generation from formal specifications of real-time reactive systems. PhD thesis, Concordia University.

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.