运行时验证
运行时验证是一种基于从运行系统中提取信息的计算系统分析和执行方法，并使用它来检测并可能对满足或违反某些属性的观察到的行为做出反应。通常需要所有系统来满足一些非常特殊的属性，例如DataRace和僵局自由，并且可以最好地实现算法。其他属性可以更方便地作为形式规格捕获。运行时验证规范通常在痕量谓词形式主义中表达，例如有限状态机器，正则表达式，无上下文模式，线性时间逻辑等或扩展。这比正常测试的临时方法更少。但是，任何监视执行系统的机制都被视为运行时验证，包括针对测试术和参考实现进行验证。提供正式的需求规格后，将监视器从它们中合成，并通过仪器在系统中注入。运行时验证可用于许多目的，例如安全或安全策略监控，调试，测试，验证，验证，验证，故障保护，行为修改（例如，恢复）等。运行时验证避免了传统正式验证技术的复杂性，例如模型检查和定理证明，仅分析一个或几个执行轨迹，并直接与实际系统合作，从而相对较好地扩展分析结果（因为它避免了乏味和错误） - 正式对系统进行建模的步骤） ，以减少覆盖范围为代价。此外，通过其反射功能，可以使运行时验证成为目标系统不可或缺的一部分，并在部署过程中监视和指导其执行。
历史和背景
对执行系统或程序进行正式或非正式指定的属性检查是一个旧主题（值得注意的示例是软件中的动态键入，或者是硬件中的故障安全设备或看门狗计时器），其精确的根源很难识别。术语运行时验证被正式引入为2001年研讨会的名称，该讲习班旨在解决正式验证和测试之间的边界问题。对于大型代码库，手动编写测试用例非常耗时。另外，在开发过程中并非所有错误都可以检测到。 Klaus Havelund和Grigore Rosu在NASA AMES研究中心进行了自动验证的早期贡献，该中心对航天器，流浪者和航空电子技术的档案高安全标准进行了档案。他们提出了一种工具来验证时间逻辑中的规格，并通过分析单个执行路径来检测Java程序中的种族条件和僵局。
当前，运行时验证技术通常会带有各种替代名称，例如运行时监视，运行时检查，运行时反射，运行时分析，动态分析，运行时/动态符号分析，跟踪分析，日志文件分析等，都参考了实例在相同的高级概念中，可以应用于不同社区的不同领域或学者。运行时验证与其他良好的领域密切相关，例如在部署前使用之前使用之前使用测试（尤其是基于模型的测试），在部署过程中使用时。
在运行时验证的广泛领域，可以区分几类，例如：
- “无规范”监视，该监视针对固定的一组主要与并发相关的属性，例如原子性。该领域的开创性工作是Savage等人的。使用橡皮算法
- 对时间逻辑规格进行监视； Lee，Kannan及其合作者以及Havelund and Rosu做出了早期的贡献。
基本方法
运行时验证方法的广泛领域可以通过三个维度进行分类：
然而，运行时验证的基本过程仍然相似：
- 通过一些正式规范创建监视器。如果在指定属性的正式语言公式中有等效的自动机，则通常可以自动完成此过程。为了转换正则表达式，可以使用有限状态的机器；线性时间逻辑中的属性可以转换为Büchi自动机（另请参见BüchiAutomaton的线性时间逻辑）。
- 该系统被仪器以将有关其执行状态的事件发送到监视器。
- 该系统已执行并由监视器验证。
- 监视器验证接收到的事件跟踪并产生是否满足规范的判决。此外，监视器还将反馈发送给系统以纠正错误行为。使用离线监视时，原因系统无法接收任何反馈，因为验证是在以后的时间点进行的。
例子
下面的示例讨论了一些在撰写本文时（2011年4月）到本文时的几个运行时验证组可能被考虑的一些简单属性。为了使它们更有趣，下面的每个属性都使用不同的规范形式主义，所有属性都是参数。参数属性是围绕使用参数事件形成的轨迹的属性，这些事件是将数据绑定到参数的事件。在这里，参数属性具有表格
update() ）是虚拟方法，这些方法不是Java API的一部分，用于清晰。
hasnext
Java 迭代器接口要求在调用next()方法之前调用hasNext()方法并返回true。如果没有发生这种情况，则用户很可能会迭代“末尾” 集合。右边的图显示了有限状态机，该机器定义了可能通过运行时验证检查和执行此属性的可能监视器。从未知状态来看，调用next()方法总是一个错误，因为这样的操作可能不安全。如果调用hasNext()并返回true ，则可以安全地调用next() ，因此监视器进入越多的状态。但是，如果hasNext()方法返回false ，则没有更多的元素，并且监视器进入无状态。在越来越多的国家中，调用hasNext()方法没有提供新的信息。可以安全地调用较大状态的next()方法，但是如果存在更多元素，则不知道该监视器会重新输入初始未知状态。最后，从无状态调用next()方法会导致输入错误状态。接下来是使用参数过去的线性时间逻辑来表示此属性的表示。
该公式说，任何对next()方法的调用都必须在返回true的hasNext()方法之前立即进行呼叫。这里的属性是迭代i中的参数。从概念上讲，这意味着测试程序中每个可能的迭代器将有一个监视器的副本，尽管运行时验证系统不需要以这种方式实现其参数显示器。该属性的监视器将设置为违反公式时触发处理程序（等于当有限状态机进入错误状态时），当next()无需先调用hasNext()或hasNext()时就会发生这种情况。 hasNext()在next()之前调用，但返回false 。
不安
Java中的 向量类有两种迭代元素的方式。如上一个示例所示，可以使用迭代器接口，或者可以使用枚举接口。除了增加迭代器接口的删除方法外，主要区别是迭代器是“快速失败”，而枚举不是。这意味着，如果一个人使用迭代器在矢量上进行迭代时修改向量（除了使用迭代器删除方法外），则会抛出consurrentModificationException 。但是，当使用枚举时，这不是一个情况，如上所述。这可能会导致程序的非确定性结果，因为从枚举的角度将向量保持在不一致的状态。对于仍使用枚举接口的旧计划，人们可能希望强制执行在修改其基础向量时未使用枚举。以下参数常规模式可用于执行此行为：
- ∀矢量V ，枚举E ：（ E = V .ELEMENT（））（ e .nextlement（）） * v .update（） e .nextlement（）
这种模式在枚举和矢量中都是参数。直观地，正如上述运行时验证系统不必以这种方式实施其参数监测器，人们可能会认为该属性的参数监视器是为每对矢量和枚举的非参数监视器实例创建并跟踪非参数监视器的实例。有些事件可能同时涉及几个监视器，例如v.update() ，因此运行时验证系统必须（从概念上）将其派遣给所有感兴趣的显示器。在此指定该属性，以说明程序的不良行为。因此，必须监视此属性的模式匹配。右侧的图显示了与此模式相匹配的Java代码，从而违反了属性。在创建枚举E之后，对向量V进行了更新，然后使用E。
Safelock
前两个示例显示有限的状态属性，但是在运行时验证中使用的属性可能要复杂得多。 Safelock属性强制执行（重点）锁定类的获取和发行次数在给定方法调用中匹配的策略。当然，这将不允许释放锁的方法，而不是获取这些锁的方法，但这很可能是测试系统实现的理想目标。以下是使用无参数上下文模式对此属性的规范：
- ∀线程T ，锁L ： S →ε| S BEGIN（ T ） S END（ T ）| s l .Acquire（ t ） s l .Release（ t ）
该模式指定每个线程的嵌套开始/结束/获取/释放对的平衡序列和锁定（ 
研究挑战和应用
大多数运行时验证研究都涉及下面列出的一个或多个主题。
减少开销的运行时
观察执行系统通常会产生某些运行时开销（硬件监视器可能会例外）。重要的是要尽可能减少运行时验证工具的开销，尤其是在系统中部署生成的监视器时。运行时额外减少技术包括：
- 改进的仪器。从执行系统中提取事件并将其发送给监视器，如果天气良好，可以生成大型运行时开销。良好的系统仪器对于任何运行时验证工具至关重要，除非该工具明确针对现有的执行日志。当前使用中有许多仪器方法，每种方法都具有其优势和缺点，从自定义或手动仪器到专门的库，再到汇编到面向方面的语言，以增强虚拟机，再到硬件支持。
-
结合静态分析。静态和动态分析的常见组合，尤其是在编译器中遇到的，是监视无法静态放电的所有要求。双重且最终等效的方法倾向于成为运行时验证的规范，即使用静态分析来减少原本详尽的监测量。可以在属性上进行静态分析以监视和监视系统。对要监视的属性的静态分析可以揭示某些事件不需要监视，因此可以延迟某些监视器的创建，并且某些现有的监视器永远不会触发，因此可以收集垃圾。监视系统的静态分析可以检测永远不会影响监视器的代码。例如，在监视上面的hasnext属性时，一个不需要仪器部分的代码部分，每个呼叫
i.next()紧接在任何路径之前，请通过calli.hasnext()返回true （在控制流图上可见）。 - 有效的监测生成和管理。当监视参数属性（如上面的示例中的参数属性）时，监视系统需要跟踪受监视属性相对于每个参数实例的状态。从理论上讲，这种情况的数量在实践中是无限的，并且往往是巨大的。一个重要的研究挑战是如何有效地将观察到的事件恰好派遣到需要它们的实例。一个相关的挑战是如何保持此类实例的数量较小（以便调度更快），换句话说，如何避免尽可能长时间地创建不必要的实例他们变得不必要。最后，参数监测算法通常会概括类似的算法来生成非参数监测器。因此，生成的非参数监测器的质量决定了所得参数监测器的质量。但是，与其他验证方法（例如，模型检查）不同，在运行时验证中，生成的监视器的大小或生成的监视器的大小不太重要。实际上，某些监视器可以具有无限的许多州，例如上面的Safelock属性的州，尽管在任何时间点都可能发生了有限数量的州。重要的是，当监视器从执行系统接收事件时，监视器从状态转移到了下一个状态。
指定属性
所有正式方法的主要实际障碍之一是他们的用户不愿或不知道也不想学习如何读取或编写规格。在某些情况下，规格是隐式的，例如用于僵局和数据率的规格，但是在大多数情况下，它们需要生产。尤其是在运行时验证的背景下，另一个不便之处在于，许多现有的规范语言不足以捕获预期的属性。
- 更好的形式主义。在运行时验证社区中，已经进行了大量的工作，以设计规范形式主义，这些形式主义适合所需的应用程序域，比传统的规范形式主义更好地适合运行时验证。其中一些包括对传统形式主义的轻微或没有句法变化，但仅是其语义的变化（例如，有限的痕量与无限的痕量语义等）以及它们的实现（优化的有限状态机器，而不是BüchiAutomata等）。其他人则扩展了现有的形式主义，其功能可用于运行时验证，但可能不容易用于其他验证方法，例如添加参数，如上所述。最后，有一些专门为运行时验证而设计的规范形式主义，试图为此域而实现最佳状态，并且对其他应用程序域的关心几乎没有关心。并将继续成为其主要的研究挑战之一，并且将继续将普遍设计更好或特定领域的更好的规范形式主义。
- 定量特性。与其他验证方法相比，运行时验证能够对系统状态变量的具体值进行操作，这使得可以收集有关程序执行的统计信息并使用此信息来评估复杂的定量属性。更需要充分利用此功能的更具表现力的属性语言。
- 更好的接口。对于非专家来说，阅读和写作属性规格并不容易。即使是专家也经常凝视着相对较小的时间逻辑公式（尤其是当他们嵌套“直到”操作员时）。一个重要的研究领域是为各种规范形式主义开发强大的用户界面，以使用户可以更轻松地理解，写作甚至可以看到属性。
- 采矿规格。无论可以使用哪种工具支持来帮助用户制作规格，他们几乎总是很高兴不得不编写任何规格，尤其是在琐碎的时候。幸运的是，那里有很多程序可以正确使用人们想要拥有的操作/事件。如果是这种情况，那么可以想像，人们希望通过自动向它们学习所需的属性来利用这些正确的程序。即使预计自动开采规格的总体质量将低于手动生产规范的总体，它们也可以作为后者的起点，也可以作为专门针对寻找错误的自动运行时验证工具的基础规格变成误报或负面因素，通常在测试过程中可以接受）。
执行模型和预测分析
运行时验证者检测错误的能力严格取决于其分析执行轨迹的能力。当将监视器与系统部署时，仪器通常是最小的，并且执行跟踪尽可能简单以保持运行时的开销低点。当使用运行时验证进行测试时，可以负担得起更全面的仪器，以增强具有重要系统信息的事件，并可以由监视器使用这些信息来构建，从而分析执行系统的更精致的模型。例如，使用向量时钟信息以及数据和控制流信息增强事件，可以使监视器构建运行系统的因果模型，在该系统中，观察到的执行仅是一个可能的实例。与模型一致的任何其他事件的排列都是系统的可行执行，在不同的线程交织下可能发生。在此类推论执行中检测违规（通过监视）使监视器预测在观察到的执行中未发生的错误，但可以在同一系统的另一个执行中发生。一个重要的研究挑战是从构成尽可能多的其他执行跟踪的执行跟踪中提取模型。
行为修改
与测试或详尽的验证不同，运行时验证具有允许系统从检测到的违规行为中恢复，通过重新配置，微分线虫或通过更精细的干预机制有时被称为调音或转向。在严格的运行时验证框架内实施这些技术会带来其他挑战。
- 动作规范。一个人需要指定要以抽象的方式进行的修改，这不需要用户知道无关的实现详细信息。另外，需要指定进行这种修改以维护系统的完整性。
- 关于干预效果的推理。重要的是要知道干预会改善情况，或者至少不会使情况恶化。
- 动作接口。与监视仪器类似，我们需要使系统能够接收动作调用。调用机制必须取决于系统的实现细节。但是，在规范级别上，我们需要通过指定在什么条件下应采用哪些操作来为用户提供对系统提供反馈的声明方式。
相关工作
面向方面的编程
运行时验证的研究人员意识到使用面向方面的编程作为一种以模块化方式定义程序仪器的技术。面向方面的编程（AOP）通常会促进横切问题的模块化。运行时验证自然就是这样关注的一个，因此可以从AOP的某些属性中受益。面向方面的监视器定义在很大程度上是声明性的，因此，与通过命令式编程语言编写的程序转换所表达的仪器相比，推理更简单。此外，静态分析可以比其他形式的程序仪器更容易地监测方面，因为所有仪器都包含在单个方面。因此，许多当前的运行时验证工具都是以规范编译器的形式构建的，它们以表达性的高级规范为输入，并以某些面向某些方面的编程语言（例如extackJ ）编写的输出代码为输出代码。
结合正式验证
运行时验证如果与可证明的正确恢复代码结合使用，则可以为程序验证提供宝贵的基础架构，从而大大降低后者的复杂性。例如，正式验证堆积算法非常具有挑战性。验证它的一种较不具有挑战性的技术是监视其输出要排序（线性复杂性监视器），如果未排序，则使用一些易于验证的过程对其进行排序，例如插入排序。结果排序程序现在更容易验证，堆件唯一需要的是它不会破坏原始元素被视为多式元素，这更容易证明。从另一个方向看，可以使用正式验证来减少运行时验证的开销，如上所述，用于静态分析而不是正式验证。实际上，可以从经过全面运行时验证，但可能会缓慢的程序开始。然后，人们可以使用正式验证（或静态分析）来放电监视器，同样的方式编译器使用静态分析来放电正确性或记忆安全的运行时检查。
覆盖范围增加
与更传统的验证方法相比，运行时验证的直接缺点是其覆盖范围降低。当运行时监视器与系统部署（以及在违反属性时要执行的适当恢复代码）时，这并不是问题的，但是当用于查找系统中的错误时，它可能会限制运行时验证的有效性。增加运行时验证的覆盖范围以实现错误检测目的的技术包括：
- 输入生成。众所周知，生成一组良好的输入（程序输入变量值，系统呼叫值，线程计划等）可以极大地提高测试的有效性。这也适用于用于错误检测的运行时验证，但是除了使用程序代码驱动输入生成过程外，在运行时验证中，也可以在可用的情况下使用属性规格，还可以使用监视技术诱导所需的行为。运行时验证的这种使用使其与基于模型的测试密切相关，尽管运行时验证规范通常是通用的，而不一定是出于测试原因而设计的。例如，考虑一下，人们想测试上面的通用不足的属性。与其仅生成上述监视器以被动地观察系统的执行，还可以生成一个智能监视器，该显示器冻结试图生成第二个E.Nextlement（）事件（在生成之前）的线程，让其他线程执行希望其中一个可以生成v.update（）事件，在这种情况下，发现了错误。
- 动态符号执行。在符号执行程序中，执行并象征性地监视，即没有具体输入。系统的一个符号执行可能涵盖大量的混凝土输入。现成的约束解决或满足性检查技术通常用于驱动符号执行或系统地探索其空间。当基本可满足性检查器无法处理选择点时，可以生成混凝土输入以通过该点； conte rete和symb olic执行的这种组合也称为共同执行。