Abstract
Real-time reactive systems are often safety-critical and hence must be thoroughly analyzed before they are deployed. This paper discusses methods for generating tests from object-oriented specifications of real-time reactive systems. Formal descriptions contain information on system entities, as mandated by requirements, as well as environmental entities, included in a domain model. These are exploited in the testing of an implementation, either for generating and sequencing tests, or as an oracle in evaluating test results. A tool has been developed based on the techniques and is being applied to several case studies developed in TROMLAB, a framework for a rigorous development of real-time reactive systems. The Train-Gate-Controller (TGC) case study presented in the paper is one of them.