论文部分内容阅读
本文介绍了一种基于自动机理论的参数化LTL公式的运行时预测监控器合成方法。参数化LTL公式是描述与系统中动态对象和数据结构相关性质的有效途径，因此本文一方面研究参数化LTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念，从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using)。另一方面给出参数化运行时监控器的概念，它由静态和动态两部分组成，静态部分由参数化b(u)chi自动机表示，动态部分为当前状态处的变量赋值。在系统运行过程中，参数化运行时监控器基于静态部分的b(u)chi自动机以及动态部分的变量赋值，以on-the-fly的方式递进的验证当前的程序运行是否满足指定的参数化性质规约。在这里参数化的运行时监控器精确识别被验证性质的最小好/坏前缀。本文同时给出参数化运行时验证器的构造和运行过程。