运行时验证工具汇总

来源自我的博客

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

运行时验证框架列举

MOP (Monitor-Oriented Programming)

面向监视的程序设计方法，对运行时验证技术进行了扩展，能够在性质满足或违反的时候作出相应的反应。基于

AOP (Aspect-Oriented Programming)

实现

LARVA

JAVA

程序的安全实时监控

RMOR (Requirement Monitoring and Recovery)

用于监控C程序的验证框架

MaC (Monitoring and Checking)

是一个通用的运行时验证框架，设计目的是确保目标程序在满足形式化需求规约前提下正确运行。它可以对任何编程语言进行验证。

Mac

验证框架使用形式化需求规约来描述待验证的性质，且其根据一个给定的需求规约自动执行插装、监控及验证。相比于

MOP

、

LARVA

等其它验证框架来说，它最大的特点是将程序监控与验证过程分享开来，从而使得高层需求规约独立于实现。

运行时验证工具列举

MOP

\

是现有的最有效最先进的运行时验证系统。

MOP

以插件的方式支持许多不同的逻辑，都使用同样的索引算法来快速访问监视器基于参数事件。一般地，

MOP

被设计来监视程序执行（在线监视）。例如，

JAVAMOP

验证由运行时

JAVA

程序生成的事件，用

ASPECTJ

仪表化。在这个评价里日志分析是在程序中插入一个日志阅读器来实现的，从日志中读入每个事件，调用给特定各类事件定义的方法，这些是空的函数体（什么都不做）。对这些空函数体方法的调用用

ASPECTJ

仪表化来驱动监视器

JavaMOP

\

一个针对

Java

的基于监控的编程(

MOP

)的软件开发和分析环境继承了

MOP

的架构，它将软件需要满足的规则以及程序的实现结合在一起。最大特点是支持多种逻辑，如上下文无关文法

CFG

、线性时序逻辑

LTL

、有限状态机

FSM

等。使用这些逻辑可以方便地对属性规范进行描述。

JavaMOP

属性规范的描述采用

mop

语法，生成的监控器代码是

AspectJ

源文件，采用

abc

编译器将

AspectJ

源文件与

Java

文件进行混合编译即可对程序进行运行时验证。使用

JavaMOP

，用户还可以实现特定的接口，定义自己的属性描述语言，具有可插拔性和灵活性。

MaC(Monitoring and Checking)

\

为程序的正确运行提供了保证，可以对目标程序进行运行时监控。

Java-MaC

是

MaC

体系的一个原型实现，可以应用于

Java

程序的运行时监控。

Java-MaC

最大的特点是较低层次的、与实现相关的程序行为的监控和较高层次的、与编程语言无关的、使用形式化描述的规范的分离。该设计使

JavaMaC

具有很强的灵活性和可扩展性。

Java-MaC

RULER

\

是一个应用于

JAVA

的运行时验证工具，创建为基于规则的系统，但和

RETE

算法相比有点小区别。

RULER

在下一步中移除了事实，除非通过规则明确指示保持它。与其相反，

RETE

只有在规则中明确指示移除事实时才会移除。

LOGSCOPE

\

是一个小规模轻量级的修改版

RULER

，强调数据参数化状态机器，应用于

SCALA

上。

LOGSCOPE

与

RULER

相反，研究的是事实的保留除非其在规则中被明确移除。

LOGSCOPE

被开发来探索语言特征且不是优化的。

TRACECONTRACT

\

一个内部的

SCALA DSL

用于状态机器，浅层的

DSL

和深层的

LTL

，也是一个简单的基于规则的符号（浅层）。应用于重写和标准化公式。

TRACECONTRACT

被开发来探索语言特征且不是优化的。

PaX

Eagle

Hawk

\

是一个基于

Eagle

的运行时验证工具。

Eagle

逻辑能够被用来定义和实现多种线性轨迹监控逻辑，采用不动点理论计算时序公式的真假。

Jass

\

是对

Java

进行运行时验证的工具，源于契约设计思想，使用注释及代码生成技术进行运行时验证。对程序的源代码有很强的依赖性。

JPaX(Java PathExplorer)

\

针对

Java

语言的运行时验证工具

TraceMatches

\

利用关于计算路径的正则表达式对

AspectJ

进行了扩展，使得多线程程序验证人员可以单独考虑单个线程或者多个线程的交叉执行。

> http://patricklam.ca/research/tracematch/

LOLA

Larva

J-LO

Temporal Rover

Conspec

MOPBox

程序静态验证系统

JML

Jahob

FindBugs

Coverity

特定领域的运行时验证工具

ARVE

Tamago

ORCHIDS

DMac

LIME

运行时验证算法实现

RETE

LOGFIRE

: 扩充了事件处理和索引方案的

RETE

算法

RETE/UL

: 添加了事件处理的对

RETE

算法的

SCALA

直接实现。

LOGFIRE

是附带有索引的此方法优化实现。

DROOLS

: 一个主要的最先进的为

JAVA

语言制订的基于规则系统，并且能免费从

JBoss

社区获取。

DROOLS

基于一个

RETE

算法的增强实现。

工具描述

Jass

和

JavaMOP

都使用了切面编程(

Aspect-oriented Programming, AOP

)技术及代码生成技术，而

Java-Mac

采用了更为精细的字节码插入技术。这3种解决方案涵盖了目前运行时验证领域里的常用技术。

MOP

支持基于自动机的验证算法。在监控器生成的初期，

MOP

将所有的非自动机的逻辑描述转化为自动机，然后生成一个监控器抽象表示，之后再生成监控器代码。

LARVA

采用时间自动机描述属性，并生成

AspectJ

监控器。

Java-MaC

与

TraceMatches

也采用类似的方法

基于公式重写的验证算法被面向规则的运行时验证技术所采用，它们一般使用公式重写的方法对有限踪迹是否满足给定的属性进行判定。

LOLA

、

Java PathExplorer

在对

LTL

属性进行监控时也采用了这样的方法。