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

摘要：

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

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

所属期刊栏目：39

分类号：TP301(计算技术、计算机技术)

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

在线出版日期：2020-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：374-378