Research Of Automated Generation Of Test Oracles From Real-Time Specification

Real-time systems have been widely used in many safety-critical areas such as aviation, spacecraft, medical treatment monitors, military command and weapon equipment control systems. In these fields, the requirements for the safety and timing constraints of real-time systems are very strict. Once some control-related errors occur at run-time, the consequence may be disastrous. So the correctness of real-time software must be guaranteed before their release. Real-time logic have obtained more and more attentions of software engineering researchers and system engineers, because their accurate syntax and semantic are able to quantitatively characterize the timing constraints of real-time systems.Due to the urgent needs for high quality software, the testing-centric quality guarantee techniques have been widely applied. Test oracle is a method for verifying whether a system under test is running as desired on a particular execution, and also an indispensable stage of software testing. However it has not been thoroughly investigated in software testing research. . This thesis proposes an approach to automatic generation of test oracle from restricted MITL (Metric Interval Temporal Logic). Firstly, a linear-causal MITL_[0, b] formula is automatically translated into a TAAS (Timed Automata with Accepting States) which acts as the test oracle using the tableau idea in model checking. Secondly, MITL_[0, b] is extended to MITL_[a, b]. The thesis proposes a method for automatic generation of test oracle based on the syntax and semantic of MITL_[a,b].The size of the state space of TAAS determines the efficiency of the run-time verification of the systems under test. The larger the state space and the transition set are, the larger the overhead of testing will be. This thesis proposes some optimized technologies for TAAS to reduce redundant and unreachable states. Moreover, an optimized refinement method is proposed for timed state sequence to reduce the extra state-interval tuples produced by the refinement.The inputs of test oracles are the traces of real-time systems. Two methods can be used to acquire the traces: one is to monitor the systems from outside, and the other is to insert assertions into the systems and observe their outputs. Each method has its advantage and weakness. The former method will not disturb the running of the systems, but it cannot acquire all the system events. The latter method does the opposite. In order to reduce or even remove the timing impact of the inserted assertions during testing, the thesis advances a new monitoring schema which has less time intrusiveness than software motoring and can test the tested system completely.