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 t...
| Main Author: | |
|---|---|
| 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. |
| Summary: | 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. |
|---|