Monitor Generation Based On Run-time Verification

Runtime verification is a lightweight verification technique which manipulates the concrete values produced by the target systems at runtime, and establishes itself as a complementary approach for classical verification techniques, such as model checking. Runtime verification has attracted more and more attention due to its effectiveness, and has already been used in many critical areas.Monitors are the core issue of runtime verification, and they are constructed form the input temporal specifications, such as linear temporal logic. Semantics of underlying temporal logics for traditional runtime verification are typically two-valued. As a results, both consistency and predictability are difficult to guarantee.We present an effective implementation of monitor generation based on some recent improvement of existing work. As the first step, we translate the input LTL formula into an alternating Büchi automation, which causes only a linear overhead in both time and space. Subsequently, the output alternating Büchi automaton is converted into a non-deterministic Büchi automaton, and the determination will be done after the prefix-recognizing transformation. Finally, the efficient monitor will be obtained by determinizing the automaton.We also propose two optimizations for Büchi automaton to reduce the scale of the generated monitor. The first one is to delete or merge some states by identifying strongly connected graph in Büchi automaton, and the second one is to remove some states of which the corresponding language is empty.Using the methods above, we have also implemented a prototype runtime verification tool which extends the JavaMOP tool, to support the construction of three-valued monitors, and conducted a series of experiments on "Maestro", which is a simulation program of NASA to study exploring on Mars, and an "lunar rover" system for the moon to verify our approach and check the correctness of our tool implementation.