面向参数化LTL的预测监控器构造方法
本文介绍了一种基于自动机理论的参数化LTL公式的运行时预测监控器合成方法。参数化LTL公式是描述与系统中动态对象和数据结构相关性质的有效途径，因此本文一方面研究参数化LTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念，从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using)。另一方面给出参数化运行时监控器的概念，它由静态和动态两部分组成，静态部分由参数化b(u)chi自动机表示，动态部分为当前状态处的变量赋值。在系统运行过程中，参数化运行时监控器基于静态部分的b(u)chi自动机以及动态部分的变量赋值，以on-the-fly的方式递进的验证当前的程序运行是否满足指定的参数化性质规约。在这里参数化的运行时监控器精确识别被验证性质的最小好/坏前缀。本文同时给出参数化运行时验证器的构造和运行过程。
运行时验证 预测监控器 自动机 变量赋值 数据结构
赵常智 董威 隋平 齐治昌
国防科学技术大学 计算机学院，湖南 长沙 410073
国内会议
沈阳
中文
221-231
2009-09-22（万方平台首次上网日期，不代表论文的发表时间）