GENERATING TEST CASES FOR REAL-TIME SYSTEMS FROM LOGIC SPECIFICATIONS

We address the problem of automated derivation of functional test case s for real-time systems, by introducing techniques for generating test cases from formal specifications written in TRIO, a language that ext ends classical temporal logic to deal explicitly with time measures. W e describe an interactive tool that has been built to implement these techniques, based on interpretation algorithms of the TRIO language. S everal heuristic criteria are suggested to reduce drastically the size of the test cases that are generated. Experience in the use of the to ol on real-life cases is reported.