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

• 作者: 叶玲玲 查显伟 钱俊彦
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: 运行时验证 JavaMOP 监控器 线性时态逻辑 Büchi自动机
• 年，卷（期）: 2019,（5）
• 页码范围: 374-378
• 页数: 5页
• 分类号: TP301
• 字数: 3396字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-808X.2019.05.006

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	钱俊彦	桂林电子科技大学计算机与信息安全学院	86	238	9.0	10.0
2	叶玲玲	桂林电子科技大学计算机与信息安全学院	1	0	0.0	0.0
3	查显伟	桂林电子科技大学计算机与信息安全学院	1	0	0.0	0.0