Abstract
Test oracles are widely used to verify whether a system under test is running as desired. Since the correctness of real-time systems depends on the logical results of the computation and the time when results are produced at the same time, an optimized model checking-based method for test oracles generation is proposed to check the system traces satisfy their real-time specifications at run time. Inspired by the idea of real-time model checking, the test oracles can be automatically generated from their specifications in the real-time logic MITL_[o, d] in a simpler way and modelled by a variant of the Timed Automata. Assertions are chosen to acquire the traces of real-time systems. A case study is presented to demonstrate the usefulness of the method proposed in this paper.