The Research Of Runtime Verification On Real-Time System

In the construction of national economy and national defense modernization, computer software become more and more popular in our daily life, people have paid attention to software reliability increasingly, especially for some safety critical areas, such as manned space flight, rail transportation and so on. Systems applied in these areas are usually real-time control systems, these systems not only require to make right response, but also require that the response satisfy corresponding time constraints. If the failure happens to the system, it will bring huge loss to national security and people, so how to improve the reliability of these systems becomes a very important research topic in computer field. Traditional test methods can’t meet the demands of the reliability of system because of incomplete test cases, model checking can give a complete proof of correctness, but for complicated systems, but it faces problems such as state space explosion. As the effective supplement of test and model checking, runtime verification implements effective monitoring and verification during system operation, and finds system failures as soon as possible, which is of great significance to improve software reliability and safety.In order to improve the safety and reliability of software, the paper proposes a runtime verification method which based on three-valued semantics of Metric Interval Temporal Logic(MITL), the contributions are:First of all, the paper introduces the syntax and semantics of MITL on finite trace over pointwise semantics, we use pointwise semantics because MITL is decidable over this semantics, and proposes the three-valued semantics of MITL on finite trace, unlike the three-valued semantics of LTL, it interprete on timed words.Secondly, the formal description of monitor which based on the three-valued semantics of MITL,transition-based generalized timed Buchi automaton(TGTBA) was proposed, it is obtained by adding clock constraints to transition-based generalized Buchi automaton(TGBA). On this basis, a construction method of an MITL-based anticipatory monitor is present, it rewrites the formula as the form required by using logic rewriting methods according to the given rewriting algorithm, generate the TGTBA based on the rewritten formula, and get the complete representation of TGTBA.Finally, based on the above verification method and MaC runtime framework, we apply the MITL-based anticipatory monitor to MaC, implement the module of property definition and monitor construction, and the validation module, consequently, a runtime verification prototype tool MITL_RV for three-valued semantics of MITL is implemented, use the tool to verify cross control system, it shows that the method this paper proposed is effective.