Improvement in JavaMOP by Simplifying Buechi Automaton

摘要

Runtime verification is a lightweight verification structure with the advantages of formal verification and software testing. In this paper, we studied JavaMOP that is an instance of the MOP (monitoring oriented programming) runtime verification structure. In the LTL plu-gin of JavaMOP, the LTL formula was translated into a nondeterministic biichi automaton (NBA) and then the NBA was translated into a deterministic finite automaton (DFA). While in the translation process, the number of states of the automata could increase exponentially. So we first use a procedure to remove the redundant states in the NBA, then we use an algorithm based on fair simulation which was used in model checking to further simplify the NBA. Experimental results show that the memory usage at runtime of JavaMOP can be reduced.