运行时验证概述

最新推荐文章于 2024-09-22 07:07:14 发布

陈止风

最新推荐文章于 2024-09-22 07:07:14 发布

阅读量2.6k

点赞数 2

分类专栏：模型检测运行时验证文章标签：测试运行时验证模型检测

本文链接：https://blog.csdn.net/yingzinanfei/article/details/54807850

版权

模型检测同时被 2 个专栏收录

5 篇文章 1 订阅

订阅专栏

运行时验证

2 篇文章 0 订阅

订阅专栏

来源自我的博客

http://www.yingzinanfei.com/2017/02/01/yunxingshiyanzhenggaishu/

运行时验证的概述

本文将简要介绍运行时验证技术。先给出运行时验证的定义，与和知名的验证技术像模型检测对比并给出测试，同时指出运行时验证的特点。然后，像面向监控编程的运行时验证扩展和基于监控的运行时反射会被简要描述并讨论他们的相同与差异。最后，指出使用运行时验证的约束。
1. 简介
  - 三种主要的验证技术：
    - 定理证明
    - 模型检测
    - 测试
  - 文章的主要内容
    - 强调运行时验证的主要思想，并且与其他验证技术相比来讨论其特点
    - 在正确属性的线性时序逻辑背景下讨论运行时验证技术
    - 总结一些用更严格更有表现力语言的扩展
    - 描述一些不仅用于监视还能在监视之下干涉系统的方法
    - 讨论对于合同使用的运行时验证技术
2. 运行时验证技术
  - “故障”定义为在当前行为和预期行为间的偏差
  - 除了传统验证技术“定理证明”、“模型检测”、“测试”，运行时检测是一个轻量级的新验证技术方向
    1. 监视器
      - 监视器是读入有限路径并生成确定结论的设备
      - 在线监视和离线监视
    2. 运行时验证与模型检测
      - 运行时验证起源于模型检测
      - 两者主要区别
      - 在模型检测中，给定系统的所有执行被用来检测其是否满足给定的正确属性 $\varphi$ ,对应于语言包含问题。而运行时检测处理的是字符问题。
      - 模型检测通常研究无穷路径，但运行时检测处理有限执行，执行也必须是有限的。
      - 模型检测中给出一个完整的模型来研究任意位置的路径，而运行时检测，特别是在处理在线监测时研究的是逐渐增大的有限执行
      - 运行时检测只处理观察到的执行，因为他是由真实系统生成的
    3. 运行时验证与测试
      - 运行时验证不研究系统所有可能的执行，这与测试有相似性
      - 两者主要区别
      - 在测试中，预言通常是直接定义的，而不是由一些高层说明生成
      - 测试穷尽一个输入集来测试系统，而运行时验证很少研究这个
      - 运行时验证可以被看作是一种“被动测试”
      - 当在最终的软件系统上加上监视器后，也可以把运行时验证理解成“永久测试”
    4. 什么时候使用运行时验证
3. 运行时验证中线性时序逻辑的说明
4. 不同层次的运行时验证的表现
5. 运行时验证之外
6. 运行时验证和合同约束
7. 结语
再探运行时验证

本文中将提出一个在线性时序逻辑LTL公式下运行时检测中的典型障碍。标准的线性时序逻辑模型是无穷轨迹的，但运行时验证只需要处理有限系统行为。这个问题通常是在给有限轨迹定义LTL语义时提出的，这和无限轨迹语义不完全契合。

我们在有限轨迹中定义一个3值语义(正确true, 错误false, 不确定inconclusive), 这样和无限轨迹最相似。此外，我们描述怎样在给定一个LTL公式后用3输出符号去构建一个确定的有限状态自动机。这个自动机输入有限轨迹然后输出他们的3值LTL语义。这样就能直接部署到运行时检测中。

我们的理念首先用在研究LTL的配置上，然后扩展到研究时间上的线性实时逻辑（简称TLTL）。因此，对于TLTL公式，监视器被构建为运行在有限时间轨迹上的。

我们应用了不定时配置并通过检查一个真实世界案例来验证整个方法。
1. 简介
  
  运行时验证作为补充像模型检测和测试这样的验证技术的工具已经越来越流行。特别是在用于模型检测不适用或不能直接适用的黑盒或灰盒系统中，或者以现在的模型检测器无法分析的系统。
2. 预备知识
  
  介绍一些关于LTL的公式定义。
3. 在不计时配置中的3值LTL
  1. 语义
  2. $LTL_3$ 的监视程序
4. 在计时配置中的3值LTL——TLTL
  1. 预备知识
  2. $TLTL_3$ 的语法和语义
  3. 事件时钟自动机
  4. $TLTL_3$ 的监视程序
5. 实现
  
  讨论怎么实现第3节中描述的不计时情况。展示实际的监视器怎么从LTL公式中自动生成，给出一个当前实现的简要概述，包括监视器生成器（简称为LTL2FSM）和一个日志框架（简称为DIAGNOSTICS）。此外，描述了我们的技术怎么用来避免一个特殊的C++陷阱，即在进入程序主函数前产生线程。
  1. 有效的监视器代码生成
  2. 我们的实现：Ltl2Fsm 和 Diagnostics
  3. 实例：静态初始化排序失败
6. 结论
  
  本文中，我们对计时和不计时的LTL关于有限轨迹都呈现了一个3值语义。我们讨论的三值语义和LTL的无限状态语义相似。
  
  此外，我们为两种逻辑都开发了有效的监视器生成程序，在一些前缀允许时能立即告警。
  
  我们已经应用了不计时的配置。我们把这个监视器生成工具整合了大型日志工具和单元测试框架。我们已经检查了一个标准C++陷阱并且对此问题提供了一个运行时验证解决方案，这个在工程上和运行时处罚上都非常有效率。
运行时验证中的LTL和TLTL

本文研究在线性时序逻辑LTL和计时的线性时序逻辑TLTL中的运行时验证属性。
1. 简介
  1. 运行时验证与模型检测
  2. 运行时验证与测试
  3. 监测离散时间属性
  4. 监测实时时间属性
  5. 概要
2. 在离散时间配置中的3值LTL
  1. 预备知识
  2. $LTL_3$ 的语法和语义
  3. $LTL_3$ 的监视器结构
  4. 举例
  5. 评价
3. 正确观察 $LTL_3$
  1. 好或坏前缀
  2. 安全与不安全属性
  3. 信息前缀
4. 在实时系统配置中的3值LTL——TLTL
  1. 预备知识
  2. $TLTL_3$ 的语法和语义
  3. $TLTL_3$ 监视的概述
  4. 运行在事件时钟自动机上的符号
  5. 符号化状态的空性检测
  6. $TLTL_3$ 的监视器程序
  7. 平台适应
5. 结论
  - 附录
  - 评价数据
基于规则的运行时验证再探
1. 简介
2. 相关工作
  1. 监视上的相关工作
  2. 规则处理上的相关工作
3. LogFire数字模拟语言
  1. 资源管理系统的需求
  2. 需求形式化成规则
    1. 事件和事实的声明
    2. 规则的通用形式
    3. 资源排序
    4. 释放需求
    5. 不释放和不准许的需求
    6. 禁止需求
  3. 监视器的终止和应用
    1. 在监视器中构成规则
    2. 应用监视器
  4. 附加特征
    1. 事件和事实
    2. 研究作为数据库的事实内存
4. 定义和使用规范模式
  1. 时序逻辑
  2. 路径表达
5. RETE算法
  1. RETE算法
  2. RETE的五个优化
    1. 规则关联
    2. 最小条件评价
    3. 前缀共享
    4. 前缀就绪
    5. 后缀就绪
6. 对运行时验证评价和修改RETE
  1. 评价
    1. 事件和事实
    2. RETE的优化
    3. 缺失的索引
  2. 修改
    1. 事件处理
    2. 索引
7. DSL(数字模拟语言)的实现
  1. 作为一等公民的名称
  2. 抽象语法规则
  3. 从具体到抽象语法
  4. 用数据可视化来理解程序
  5. 测试
  6. 文档
8. 实验
  1. 系统比较
    - LOGFIRE: 本文介绍的基于规则的系统，是扩充了事件处理和索引方案的RETE算法
    - RETE/UL: 添加了事件处理的对RETE算法的SCALA直接实现。LOGFIRE是附带有索引的此方法优化实现。
    - DROOLS: 一个主要的最先进的为JAVA语言制订的基于规则系统，并且能免费从JBoss社区获取。DROOLS基于一个RETE算法的增强实现。
    - RULER: 是一个应用于JAVA的运行时验证工具，创建为基于规则的系统，但和RETE算法相比有点小区别。RULER在下一步中移除了事实，除非通过规则明确指示保持它。与其相反，RETE只有在规则中明确指示移除事实时才会移除。
    - LOGSCOPE: 是一个小规模轻量级的修改版RULER，强调数据参数化状态机器，应用于SCALA上。LOGSCOPE与RULER相反，研究的是事实的保留除非其在规则中被明确移除。LOGSCOPE被开发来探索语言特征且不是优化的。
    - TRACECONTRACT: 一个内部的SCALA DSL用于状态机器，浅层的DSL和深层的LTL，也是一个简单的基于规则的符号（浅层）。应用于重写和标准化公式。TRACECONTRACT被开发来探索语言特征且不是优化的。
    - MOP：是在我们认识内现存的最有效最先进的运行时验证系统。MOP以插件的方式支持许多不同的逻辑，都使用同样的索引算法来快速访问监视器基于参数事件。一般地，MOP被设计来监视程序执行（在线监视）。例如，JAVAMOP验证由运行时JAVA程序生成的事件，用ASPECTJ仪表化。在这个评价里日志分析是在程序中插入一个日志阅读器来实现的，从日志中读入每个事件，调用给特定各类事件定义的方法，这些是空的函数体（什么都不做）。对这些空函数体方法的调用用ASPECTJ仪表化来驱动监视器
  2. 特定的需求
  3. 日志
  4. 结果
9. 结论和未来工作
运行时验证框架MOP概述

本文给出了关于面向监视的程序框架MOP的概述。在MOP中支持运行时监视并且被支持作为一个基本原则来构建可依赖系统。监视器自动地综合特定属性并连同原始系统来检测动态行为。当一个规范违反或运行时验证时，用户定义的行为会触发，这个可以是任何代码像信息日志记录或运行时恢复。两个MOP的实例将会介绍：JavaMOP（适用于Java程序）和BusMOP（适用于监视PCI总线流量）。MOP的架构也会被讨论，参数轨迹监视和应用实施将被给出。JavaMOP的综合评价证实了它的效率，特别是和类似的系统相比。BusMOP的细节实现将被讨论。通常BusMOP在其监视系统时不会有额外的系统运行开销。
1. 简介
  1. 相关工作
    1. 面向方向的编程语言
    2. 运行时验证
    3. 契约式设计
    4. 其他相关的方法
    5. 讨论
  2. 举例
2. MOP框架
  1. 架构
  2. 语言客户端
  3. 逻辑插件
3. MOP实例
  1. MOP语法
    1. 共享的语法
    2. 特殊实例的语法
    3. 特殊逻辑插件的语法
  2. JavaMOP实例
    1. JavaMOP语法
  3. BusMOP实例
    1. BusMOP语法
4. JavaMOP
  1. 参数轨迹切片和朴素监视
    1. 事件、轨迹、属性和参数
    2. 监视器和参数监视器
    3. 朴素参数监视
  2. 有效地参数监视
    1. 算法C<X>
    2. 启用优化
    3. 算法D<X>
  3. 索引
    1. 集中化索引
    2. 优化：分散化索引
  4. 结合模型和关联
5. BusMOP
  1. PCI总线
  2. 监视设备
    1. PCI核心模块
    2. 第N系统模块
    3. 总结接口模块
    4. 监视器模块
  3. BusMOP评价
6. 逻辑插件
  1. 有限状态机器
  2. 扩展正则表达式
  3. 线性时序逻辑（未来时间）
  4. 过去时间线性时序逻辑
  5. 上下文无关文法
  6. 过去时间线性时序逻辑的调用与返回
7. 结论