模型检查

本文是关于检查计算机科学模型的。有关统计中模型的检查，请参见统计模型验证。
可以检查电梯控制软件以验证这两个安全性能，例如“机舱永远不会开门” ，并且每当按下n层的呼叫按钮时，livese的特性，例如”，机舱最终将在N楼层打开门” 。

在计算机科学中，模型检查或属性检查是一种检查系统的有限状态模型是否符合给定规范（也称为正确性）的方法。这通常与硬件或软件系统相关联，该规范包含LIVISICE要求（例如避免生计）以及安全要求（例如避免代表系统崩溃的状态）。

为了以某种精确的数学语言制定了系统的模型及其规范。为此，该问题是作为逻辑任务提出的，即检查结构是否满足给定的逻辑公式。这个一般概念适用于多种逻辑和多种结构。一个简单的模型检查问题包括验证给定结构是否满足命题逻辑中的公式。

概述

当两个描述不等效时，属性检查用于验证。在细化过程中，规范补充了高级规范中不需要的细节。由于不可能，因此无需针对原始规范验证新引入的属性。因此，严格的双向等价检查放宽到单向属性检查。实现或设计被视为系统的模型，而规格是该模型必须满足的属性。

已经开发了一类重要的模型检查方法，用于检查硬件和软件设计模型，其中规范由时间逻辑公式提供。时间逻辑规范的开创性工作是由Amir Pnueli完成的，他因“将时间逻辑引入计算科学介绍”而获得了1996年的Turing奖。模型检查始于JP Queille和J. Sifakis的Em Clarke ， Ea Emerson的开创性工作。克拉克（Clarke），艾默生（Emerson）和西法基斯（Sifakis）因其开创性的工作创始和开发模型检查领域而获得了2007年的图灵奖。

模型检查最常应用于硬件设计。对于软件，由于不可证明性（请参阅计算性理论），该方法不能完全算法，适用于所有系统，并始终给出答案；在一般情况下，它可能无法证明或反驳给定财产。在嵌入式系统硬件中，可以通过UML活动图或控制解干的PETRI网验证提供的规范。

该结构通常以工业硬件说明语言或特殊用途语言为源代码描述。这样的程序对应于有限状态计算机（FSM），即，由节点（或顶点）和边缘组成的有向图。一组原子命题与每个节点相关联，通常说明哪些内存元素是一个。节点代表系统的状态，边缘代表可能改变状态的可能过渡，而原子命题则代表在执行点所持的基本属性。

正式地，问题可以说如下：给定所需属性，以时间逻辑公式表示和一个结构具有初始状态 ，确定是否 。如果是有限的，就像在硬件中一样，模型检查还原为图形搜索。

符号模型检查

与其一次列举可及的状态，有时可以通过在一个步骤中考虑大量状态来更有效地遍历状态空间。当这种状态空间遍历基于一组状态和过渡关系的表示，二进制决策图（BDD）或其他相关数据结构时，模型检查方法是象征性的。

从历史上看，第一个符号方法使用了BDD 。在解决人工智能中的计划问题（请参阅Satplan ）中，命题令人满意成功之后，将同样的方法推广以模型检查线性时间逻辑（LTL）：计划问题对应于模型检查安全性能。此方法称为有界模型检查。在有限的模型检查中，布尔满意度求解器的成功导致符号模型检查中的满意度求解器的广泛使用。

例子

这样的系统要求的一个例子：在地板上调用电梯的时间到该地板上的门时，电梯最多可以到达该地板两次。 “有限国家验证的属性规范中的模式”的作者将此要求转化为以下LTL公式：

这里， 应该读为“始终”， 作为“最终”， 作为“直到”，其他符号是标准逻辑符号， 对于“或”， 对于“和”和对于“不”。

技术

模型检查工具将面临状态空间的组合炸毁，通常称为状态爆炸问题，必须解决该问题以解决大多数现实世界中的问题。有几种解决这个问题的方法。

  1. 符号算法避免明确构建有限状态机（FSM）的图形；相反，它们在量化的命题逻辑中使用公式隐式表示图。二进制决策图（BDD）的使用受到肯·麦克米兰（Ken McMillan）的作品以及开源BDD操纵库（例如Cudd and Buddy）的开发。
  2. 有限的模型检查算法在固定数量的步骤中展开FSM， 并检查是否可能发生财产违反财产或更少的步骤。这通常涉及将限制模型编码为SAT的实例。可以使用越来越大的值重复该过程直到排除所有可能的违规行为（参见迭代深度深度搜索）。
  3. 抽象试图通过首先简化系统来证明系统的属性。简化的系统通常不满足与原始系统完全相同的属性，因此可能需要进行改进的过程。通常，一个人需要抽像是声音的（原始系统中的抽象性属性是正确的）；但是，有时抽像不完整（并非原始系统的所有真实属性在抽像中都是正确的）。抽象的一个例子是忽略非树状变量的值，而仅考虑布尔变量和程序的控制流。这种抽象尽管看起来很粗糙，但实际上可能足以证明相互排斥的特性。
  4. 反例引导的抽象细化（CEGAR）开始用粗糙（IE不精确）的抽象进行检查，并迭代地完善它。当发现违规行为（即反例）时，该工具将其分析以确保可行性（即，违规是真实的还是不完全抽象的结果？）。如果违规是可行的，则将其报告给用户。如果不是这样，则使用不可行的证明来完善抽象，然后重新开始检查。

最初开发了模型检查工具是为了理解离散状态系统的逻辑正确性，但此后已扩展以处理实时和有限形式的混合系统。

一阶逻辑

在计算复杂性理论领域还研究了模型检查。具体而言，一阶逻辑公式是固定的，没有自由变量，并且考虑了以下决策问题：

例如，给定有限的解释，例如一种被描述为关系数据库的解释，决定解释是否是公式的模型。

此问题在电路类AC 0中。当对输入结构施加一些限制时，它是可以处理的：例如，要求它具有由常数界定的树宽度（通常意味着模型检查Monadic二阶逻辑的障碍性），以每个域元素的程度，界定每个域元素的程度，以及更一般的条件，例如有限的扩展，局部界限的扩展以及无处可信的结构。这些结果已扩展到将所有解决方案列举为具有自由变量的一阶公式的任务。

工具

主要文章：模型检查工具列表

这是重要的模型检查工具的列表：

  • AFRA： Rebeca的模型检查器，这是一种基于演员的语言，用于建模并发和反应性系统
  • 合金（合金分析仪）
  • Blast （伯克利懒惰抽象软件验证工具）
  • CADP （分布式流程的构建和分析）用于设计通信协议和分布式系统的工具箱
  • CPACHECKER ：基于CPA框架的开源软件模型检查器
  • Eclair ：C和C ++程序的自动分析，验证，测试和转换的平台
  • FDR2 ：用于验证实时系统建模和指定为CSP过程的模型检查器
  • MPI程序的ISP代码级验证程序
  • Java Pathfinder ：Java程序的开源模型检查器
  • LIBDMC ：分布式模型检查的框架
  • MCRL2工具集，基于ACP的增强软件许可证
  • NUSMV ：新的符号模型检查器
  • PAT ：增强的模拟器，模型检查器和改进检查器，用于并发和实时系统
  • 棱镜：概率符号模型检查器
  • Roméo ：用于建模，模拟和验证的集成工具环境，以参数，时间和秒表彼得里网建模
  • 旋转：一种以严格且主要是自动化的方式验证分布式软件模型正确性的一般工具
  • 风暴：概率系统的模型检查器。
  • 小吃：分析过程代数的工具
  • Tapaal ：用于建模，验证和验证定时ARC Petri网的集成工具环境
  • TLA+型号检查器Leslie Lamport
  • Uppaal ：用于建模，验证和验证的集成工具环境，该系统模型为定时自动机网络
  • Zing - 从微软到各个级别的软件状态模型的实验工具：高级协议描述，工作流规范，Web服务，设备驱动程序和操作系统核心中的协议。 Zing目前正在用于开发Windows驱动程序。

也可以看看