基于Büchi自动机化简的JavaMOP监控器构造方法

The overhead control on monitor of JavaMOP based on Büchi automata simplification

为了提高JavaMOP对程序运行时验证的效率,提出一种基于Büchi自动机化简的JavaMOP监控器构造方法,降低JavaMOP运行时验证的时间和内存开销。该方法将线性时态逻辑(linear temporal logic,简称LTL)描述的属性规范转化为Büchi自动机,利用自动机化简规则对Büchi自动机进行冗余化简,化简后的Büchi自动机再转化为确定性有限自动机,并由此得到监控器的抽象表示。实验结果表明,与JavaMOP现有监控器的方法相比,该方法能够得到更小的Büchi自动机,从而加速JavaMOP监控器的构造过程。

In order to improve the monitored efficiency of JavaMOP in runtime verification,a method based on Büchi automata simplification to build monitor is proposed,which reduces the overhead of JavaMOP runtime verification.This method first translates the properties described by LTL(linear temporal logic)into Büchi automata,and utilizes the reduction rules for automaton to prune the redundant states,then the simplified Büchi automata are converted into determine finite automata(DFA)to obtain the abstract representation of the monitor.Experimental results show that the proposed method can gain smaller Büchi automata and accelerate the process of constructing the monitor in JavaMOP.