面向参数化LTL的预测监控器构造技术

• 作者: 董威 赵常智 隋平 齐治昌
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 运行时验证 软件监控 预测监控器 参数化LTL(linear temporal logic) 参数化Büchi自动机
• 年，卷（期）: 2010,（2）
• 页码范围: 318-333
• 页数: 16页
• 分类号: TP311
• 字数: 16587字
• 语种: 中文

摘要

介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称PALTL)公式运行时预测监控器构造方法.一方面研究PALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using);另一方面给出参数化预测监控器的概念.它由静态和动态两部分组成,静态部分由参数化Büchi自动机表示,动态部分为当前状态处的变量赋值.在系统运行过程中,预测监控器基于静态部分的参数化Büchi自动机,以on-the-fly的方式在当前状态处动态地提取和绑定变量赋值,递进地验证当前程序运行是否满足指定的参数化性质规约.在该过程中,参数化监控器能够精确地识别被验证性质的最小好/坏前缀.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董威	国防科学技术大学计算机学院	32	402	10.0	19.0
2	齐治昌	国防科学技术大学计算机学院	38	881	15.0	29.0
3	赵常智	国防科学技术大学计算机学院	4	24	3.0	4.0
4	隋平	国防科学技术大学计算机学院	3	18	2.0	3.0