Specification-based testing for real-time reactive systems

We describe methods for specification based testing and testing measurement for real time reactive systems. The methods are based on an object oriented formal specification of real time reactive systems. Test cases generated by our method satisfy two test adequacy criteria, and minimally cover the global states and transitions of interest. The testing measurement provides measures of test suite adequacy in terms of coverage. We use a metric based algorithm to select the optimal set of test cases. One of the goals of this work is to automate these methods and integrate them into TROMLAB, a rigorous framework for the development of real time reactive systems