The Study Of Monitor Optimization Method Based On Runtime Verification

With the increasing scale and complexity of computer software systems,it is more and more difficult to verify the security and reliability of the software systems,the traditional verification techniques have been unable to meet the demand.Runtime verification,a lightweight verification technique,which is used to improve the security and reliability of software systems,it is an effective supplement to the traditional verification techniques and it verifies whether the software system is correct by monitoring the actual running state of software system.However,in runtime verification,monitoring the running state of software system could cause some additional runtime overhead,which impacts on the performance of software system.Therefore,it is an important research to reduce the runtime overhead in the field of runtime verification.This paper focues on how to reduce the overhead of runtime verification efficiently,and our work is mainly concentrated on JavaMOP,which is a runtime verification tool.We reduce the time and memory consumption of JavaMOP and improve the efficiency of JavaMOP by optimizing JavaMOP.In this paper,we first analyze the process of constructing monitors when JavaMOP verifies the Linear temporal logic(LTL)properties,and an improved method of constructing monitor is proposed and studied.This method uses transition-based generalized Büchi automaton(TGBA)as an intermediate auxiliary automaton.First,converting LTL properties into TGBA directly,and simplifying TGBA;then degeneralizating the simplified TGBA into Büchi automata;in the last,obtaining determining finite automata from Büchi automata that is the abstract representation of the monitors.The experimental results show that this method can get smaller Büchi automata,accelerate the process of constructing monitors,and reduce the time and memory overhead of generating monitors in JavaMOP.For runtime verification of parametric properties,we combine the static analysis technique with garbage collection mechanism to analyze the monitor instances that verify parametric properties,so that reduces some unnecessary monitor instances in the process of monitoring and further decreases the overhead of runtime verification.The parametric properties provide a good way to describe the behavior of object-oriented system.When JavaMOP verifies parametric properties,the parameters are bound to the specific object instances,then the corresponding monitor instances are generated to monitor parametricproperties.In this paper,the Sufenable Set is proposed by combining with static analysis technique to collect and analysis useless monitor instances during monitoring parametric properties,then the unnecessary monitor instances are recycled and released.Meanwhile,we reduce the magnitude of system monitoring and monitor instrumentation by pre-processing system before verifying the system,thereby reducing the overhead of runtime monitoring.