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

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

作　　者：叶玲玲 钱俊彦 查显伟 YE Lingling;QIAN Junyan;ZHA Xianwei(School of Computer and Information Security,Guilin University of Electronic Technology,Guilin 541004,China)

机构地区：[1]桂林电子科技大学计算机与信息安全学院

出　　处：《桂林电子科技大学学报》2019年第5期374-378,共5页Journal of Guilin University of Electronic Technology

基　　金：国家自然科学基金(61562015);广西自然科学基金(2018GXNSFDA138003);桂林电子科技大学研究生教育创新计划(2017YJCX51)

摘　　要：为了提高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.

关 键 词：运行时验证 JavaMOP 监控器 线性时态逻辑 BÜCHI自动机 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]