运行时验证

运行时验证是一种计算系统分析和执行方法，它基于从运行中的系统中提取信息，并利用它来检测和可能对观察到的满足或违反某些属性的行为作出反应。

一些非常特殊的属性，如数据流和死锁自由，通常希望所有系统都能满足，并且可能xxx以算法方式实现。其他属性可以更方便地被捕获为形式化规范。

运行时验证规范通常用跟踪谓词形式表达，如有限状态机、正则表达式、上下文自由模式、线性时间逻辑等，或这些的扩展。这允许采用比正常测试更少的临时性方法。然而，任何监控执行系统的机制都被认为是运行时验证，包括针对测试神谕和参考实现的验证。当提供正式的需求规格时，监控器是由它们合成的，并通过仪器的方式注入系统中。

运行时验证可用于许多目的，如安全或安全策略监控、调试、测试、验证、确认、剖析、故障保护、行为修改（例如，恢复）等。

运行时验证避免了传统形式验证技术的复杂性，如模型检查和定理证明，它只分析一个或几个执行轨迹，并直接与实际系统一起工作，因此扩展性相对较好，对分析结果更有信心（因为它避免了对系统进行形式化建模的繁琐和容易出错的步骤），但代价是覆盖面较小。此外，通过其反射能力，运行时验证可以成为目标系统的一个组成部分，在部署期间监控和指导其执行。

对执行中的系统或程序进行正式或非正式的属性检查是一个古老的话题（值得注意的例子是软件中的动态类型，或硬件中的故障安全装置或看门狗定时器），其确切的根源很难确定。

术语"运行时验证"是在2001年的研讨会上正式提出的，旨在解决形式验证和测试之间的问题。对于大型代码库，手动编写测试用例是非常耗时的。

此外，并不是所有的错误都能在开发过程中被发现。KlausHavelund和GrigoreRosu在NASAAmes研究中心对自动化验证做出了早期的贡献，为航天器、漫游车和航空电子技术的高安全标准存档。

他们提出了一个工具来验证时间逻辑的规范，并通过分析单一的执行路径来检测Java程序中的竞赛条件和死锁。

目前，运行时验证技术经常以各种不同的名称出现，如运行时监控、运行时检查、运行时反射、运行时分析、动态分析、运行时/动态符号分析、跟踪分析、日志文件分析等，都是指应用于不同领域或由不同社区的学者提出的同一高层概念的实例。

运行时验证与其他成熟的领域密切相关，如在部署前使用的测试（特别是基于模型的测试）和在部署期间使用的容错系统。在广泛的运行时验证领域，我们可以区分几个类别，例如。无规范的监控，其目标是一套固定的主要与并发性有关的属性，如原子性。

这一领域的开创性工作是Savage等人的Eraser算法对时间逻辑规范的监控；Lee、Kannan和他们的合作者以及Havelund和Rosu也在这一方向做出了早期贡献。基本方法运行时验证方法的广泛领域可以按三个方面进行分类。

系统可以在执行过程中被监控（在线）或在执行后被监控，例如以日志分析的形式（离线）。验证代码被集成到系统中（如面向方面的编程）或作为一个外部实体提供。

监控器可以报告违反或验证所需的规范。然而，运行时验证的基本过程仍然相似。从一些形式化的规范中创建一个监 视器。如果有等价的自动机用于指定属性的形式化语言的公式，这个过程通常可以自动完成。

为了转换正则表达式，可以使用有限状态机；线性时态逻辑中的属性可以转换为Büchi自动机。系统被设置为向监 视器发送有关其执行状态的事件。