理论计算机科学电子笔记274（2011）3-16www.elsevier.com/locate/entcs动态路径缩减SebastianBiallas1J？orgBrauer1 DominiqueGu？ckel2Stefan Kowalewski1德国亚琛工业大学嵌入式软件实验室摘要路径约简是一种著名的技术，以减轻显式状态模型检测引起的状态爆炸问题，其核心思想是存储状态只在预定的断点。本文提出了一种适应这种技术，检测断点上的状态空间生成过程中的-crossy。该方法特别适用于静态分析产生粗过近似的系统中的断点检测。我们通过将其应用于二进制代码验证来评估这种技术的有效性。保留字：验证，模型检验，状态爆炸，路径约简1引言尽管对抽象进行了大量的研究，但状态爆炸仍然是（显式状态）软件模型检查适用于现实世界应用的主要障碍[5]。CTL模型检查的一个这样的抽象是所谓的路径缩减[18]。 路径约简的关键思想是将单个的-状态空间中的后继链，如果中间状态不能影响指定的有效性。这意味着只有在访问导致状态空间中的分支或影响CTL规范。这些程序位置称为断点。比如说，改变原子命题中使用的变量的值或读取非确定性值的程序语句仅在这些特定位置存储状态减少了状态空间的内存占用，可能以增加运行时间为代价1电子邮件：{lastname}@ embedded.rwth-aachen.de2电子邮件：gueckel@embedded.rwth-aachen.de1571-0661 © 2011由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2011.07.0034S. Biallas等人/理论计算机科学电子笔记274（2011）3在他们的开创性论文中，Yorav和Grumberg [18]描述了使用静态分析检测模型检查器Mur的断点。由于在Mur中使用的输入语言的相当有限的性质，断点可以对于这种特殊的工具，必须准确地确定。然而，情况并非总是如此。这种方法可能导致粗略过度近似的一个领域是嵌入式系统的二进制代码验证[13，14]。这有不同的原因，例如：• 低级平台的程序通常是中断驱动的。在这种情况下，状态必须存储在中断可能触发的任何程序位置，因为中断处理程序的执行是可选的，因此会导致状态空间的分裂。• 非确定性通常通过硬件本身引入。读取同一个寄存器（比如输入端口）的值可能会导致确定性或非确定性值，具体取决于确切的硬件配置。不幸的是，没有已知的静态分析技术可以如所需的那样精确地推断硬件的状态。• 为了保证模型检查过程的终止，状态需要存储在可能的非终止循环中（对于固定点检测）。因此，每个环中至少有一个位置必须断开。尽管在高级程序的终止证明方面取得了进展[7]，但这些技术还不适用于低级代码。因此，基于静态分析的二进制代码模型检查的路径缩减没有达到其他领域已知的有效性[14，Sect.6.2]。然而，二进制代码模型检查器通常使用目标微控制器的专用模拟器来生成状态空间。因此，在状态空间构建期间，微控制器的确切配置是已知的。例如，当模拟间接存储指令时，该指令的具体目标地址是已知的，并且断点检测不必依赖于保守的过近似。我们在这篇论文中的主要贡献是一种新的技术，称为对的路径减少，动态执行状态空间减少，而状态空间的建立（见节。2）。这种技术是新颖的，因为它执行的任务，在生成状态的同时检测固定点。我们还详细介绍了如何将路径约简得到的反例扩展为具体的反例[3，6]（见第3节）。为了评估的有效性上的-的路径减少，我们将其性能进行比较，使用静态检测的断点在节中获得的结果。四、最后，Sect。5介绍了相关的工作和节。6、结束论文。2减少路径上的不确定性我们通过静态分析实现了路径约简（SPR），并为我们用于案例研究的模型检查器[MC]SQUARE[13]实现了新的本节详细介绍了算法的动机和实现。S. Biallas等人/理论计算机科学电子笔记274（2011）35一BCDeFGH我JKLMn一CFn2.1预赛[MC]SQUARE使用根据[8]的在线模型检查算法。这意味着状态空间是即时生成的：状态对应于微控制器的配置，如果模型检查器需要跟踪尚未创建的后续状态的路径约简算法需要处理状态的实时生成。 也就是说，不是通过执行单个指令来返回直接后继，模拟器应该遵循返回应该出现在缩减的状态空间中的下一个状态的后续指令的路径。是什么让一个国家成为下一个状态（并因此确定缩减的状态空间）需要以某种方式这种归约是无法用CTL−X逻辑区分的。这里，CTL-X表示没有下一次运算符X的逻辑CTL，其不能用于缩减状态空间。我们把符合这样一个标准的状态称为新的继承国崩溃。路 径 （a，b1，b2，. ，b，n，c），其中至多a和c是断裂的称为基本路。因此，约简状态空间中的每个跃迁对应于原始状态空间中的一条基本路径。作为示例，图1示出了具有标记为a至n的14个状态的状态空间。图2中示出了相应的缩减状态空间。虽然只剩下四个断裂状态a，c，f和n，但状态空间与原始状态空间是断续的双相似[2，16]。这是通过将中间状态只有一个后继的基本路径（如（c，e，i，n））合并为单个转换（c，n）来实现的。注意，这样的状态修剪对于像（c，d，h，m，l，c）这样的被合并到转变（c，c）中的循环也是可能的还要注意，状态b没有出现在缩减的状态空间中，尽管它有两个前导。然而，循环（f，j，g，k，f）需要特殊处理，因为它的状态都没有多个后继。我们现在将评估一个状态被破坏的标准，即。例如， 出现在简化的状态空间中。对于SPR，该标准仅取决于程序计数器。在这里，中断程序位置（中断点）是使用静态Fig. 1. 示例状态空间图2. 应用路径缩减6S. Biallas等人/理论计算机科学电子笔记274（2011）3分析.之后，对于具有匹配这些值的程序计数器的每个状态，路径修剪算法在状态空间生成期间停止。静态分析[18，14]选择每个位置作为断裂点，• 其中可以触发不确定性中断，或者• 当从输入寄存器读取时，对应的指令执行一些非确定性操作，或者• 其中相应的指令改变了在CTL公式中用作原子命题的变量（内存位置）的值，或者• 其是跳转（或其它控制转移）指令的目标。前两个条件使位置中断，其中对应的状态在状态空间中有多个后继第三个条件保证公式中使用的变量的所有更改对模型检查器可见最后，第四个条件确保程序中的每个循环都存在断点，这样状态空间中的每个循环都至少有一个断点检测的断点状态。正如在引言中提到的，使用静态分析来确定断裂点通常会产生粗略的过度近似，从而假设比必要的更多的断裂位置。例如，在I/O端口上的读操作，isconfidence for input返回一个不确定的值，这反过来又导致状态空间中的分支。相应的程序位置因此被标记为中断。然而，I/O端口也可以被配置为输出，这意味着它存储确定性值。在这种情况下，相应的程序位置不需要中断。由于静态分析无法准确捕获硬件的这种位级依赖性，因此它计算出的结果过于悲观。此外，第四个条件使得不可能将程序的长时间运行循环修剪成单个转换。在下一小节中，我们将重点介绍新的OPR，它使用可以实时评估的标准来确定状态是否正在中断，从而可以处理这些问题。2.2在线路径约简OPR的一般思想是，我们通过评估其局部邻域来确定每个状态（而不是每个程序位置）是否中断。这个决定是在状态空间生成过程中做出的，因此我们需要可以即时检查的条件：当沿着基本路径生成状态时，OPR假设一个状态是中断的，如果• 它有一个以上的继承人，或• 一个原子命题的真值在转换到它的（唯一）后继命题之后发生变化，或者• 它已经在这条基本的道路上被访问过了。第一个条件确保必须采取非确定性决策的状态（例如执行中断或从硬件寄存器读取S. Biallas等人/理论计算机科学电子笔记274（2011）37出现在状态空间中为了保持所有修改对模型检查器的可见性，第二个条件确保在每个基本路径中最多有一个转换可能与公式相关联。最后一个标准需要保证终止性，稍后将详细研究。首先，我们正式描述OPR后继状态生成的算法：算法1在约简状态空间中生成状态后继输入：sourceState输出：缩减状态空间中sourceState的后继1：successors←继承DirectSuccessors（sourceState）2：resultSuccessors← {}3：对于所有状态的后继者，4：当前←状态5：访问←{}6：重复7：visited←visited{current}8：nextStates创建DirectSuccessors（currentState）9：next∈nextStates10：打破←|下一个国家|/= 1 or atomics（current）11：如果不打破，12：当前←下一个13：如果结束14：直到断开或电流∈访问15：resultSuccessors←resultSuccessors{current}十六： 端17：returnresultSuccessors原子学（下）对于每个直接后继，算法的内部循环（第6在下一节中，将描述如何实现第7行和第14行中的环路检测，其用于满足用于断开状态的第三条件。2.3循环检测我们描述了三个不同的标准，用于检测基本路径中的循环，可以一次性检查：• 如果两次遇到相同的程序计数器，则停止。• 如果遇到两次相同的状态，则停止。• 如果两次遇到同一个状态的哈希代码，则停止第一个标准受到SPR的启发，并保证每个循环（在程序中，因此在状态空间中）至少包含一个中断指令。缺点是，没有非确定性控制流的每个循环（例如，存储器复制或初始化）将在状态空间中创建至少一个状态，8S. Biallas等人/理论计算机科学电子笔记274（2011）3每次迭代。为了修剪这样的循环，第二个标准考虑了整个微控制器的配置，也就是说，沿着基本路径的所有状态都被临时存储，并且假设状态已经在这个列表中中断一次。由于状态的大小是有限的，因此保证所有循环都终止。这将控制流中的循环与状态空间中的循环分开，因此允许将循环表示为单个转换。第三个标准是第二个标准的改进。 它只需要原始状态数据的64位哈希码作为检测已经遇到的状态的标准。这是更快和更少的内存密集型，因为只有所有中间状态的散列必须被存储，而模拟沿一个基本路径。正如我们的案例研究将显示，第三个标准oesperers的高精度，同时是一个非常快的可能性，以检测在状态空间中的循环总而言之，到目前为止介绍的OPR的优点是：• 不需要静态分析，这会产生更准确的结果。• 我们的算法是独立的用于状态生成的微控制器模拟器。另一方面，对于SPR，微控制器的详细知识对于检测断开状态是必要的。• 可以将具有许多迭代的程序循环修剪成单个转换。虽然本节讨论了减少路径以缓解状态爆炸，但我们将在下一节中讨论如何重新扩展路径以创建有意义的反例。3扩充反例反例/见证是状态空间中的路径（可能带有循环），显示如何达到某些不期望的属性或从未达到某些期望的属性。反例提供了重要的信息，以帮助理解为什么公式是有效的或违反[4]。例如，公式AG x= 5的一个反例将显示一条通向x等于5的状态的路径（以及所有非确定性输入）。另一方面，公式AF x= 6的一个反例将显示一条进入循环的路径，使得x= 6永远无效。在简化的状态空间中，反例不太有用。为了说明，考虑图3，其中示出了反例迹线（a，c，d）;该公式在状态下为假。D. 通过路径简化省略的状态（b和bJ）被示出为虚线圆。到为了理解这样的反例轨迹，关键是要知道对于（a，b）过渡采取了哪不幸的是，这种信息不容易从反例迹线中可见的（a，c）跃迁中获得：状态c可能太远而无法在没有人工调查的情况下区分（a，b）跃迁和（a，bJ为了解决这个问题，我们实现了通过重新扩展所有约化路径来反转路径约化对[MC]SQUUARE中给定反例迹的效应的这样的重新扩展的反例然后与它们的对应的S. Biallas等人/理论计算机科学电子笔记274（2011）39原始状态空间中的轨迹。这是通过两个步骤实现的。在第一步中，使用模拟器重新创建路径简化忽略的所有状态。对于只有一个后继者的状态，创建直接后继者直到到达缩减路径上的下一个状态是足够的。然而，对于有不止一个继承者的状态，我们必须找出哪个过渡实际上属于反例。这对应于图3中的（a，b）和（a，b，J）转变之间的决定。为了决定这些不确定性转换中的哪一个属于反例，在节点a处开始对目标状态c的广度优先搜索。当找到状态c时，搜索终止。有多个继承者的状态不需要被跟踪，因为它们是中断的，因此是减少的状态空间的一部分。 通往c国的道路 然后添加到反例中，使不确定性决策变浅。在第二步中，状态在基本路径的末端被丢弃，其中违反公式在第一次转换中表现出来，但在这条路径的末端被注意到，这种情况在图4（上半部分）中描述。让我们假设在（a，b）转换之后，公式被违反，i。e. 该公式在状态a中为真，但在状态b到c中为假（回想一下，仅第一个过渡可能会影响公式）。由于只有a和c被存储在缩减的状态空间中，而其间的状态被省略，因此在状态c中检测到公式的违反，产生以c结尾的反例。最好有最短的反例（突出显示使公式无效的第一条指令），因此我们将状态b降为c。 正式地说，一条以（...，a，c）的简化反例转化为（.，a，b），其中b是原始状态空间中a的直接后继者。这在图的下部示出。四、路径简化的另一个缺点是CTL的X运算符丢失。当我们在机器指令级别上执行模型检查时，X运算符无论如何都没有实际意义4案例研究本节描述了不同的实验，以检查OPR对不同评估标准的影响：检测（见4.1节），与基于静态分析的路径简化的比较（见4.2节），以及CTL规范对生成的状态空间的影响（见4.3节）。所有实验均在配备有Sun Fire X4600 M2服务器的设备上运行。......TT TT ...TT FF图三.反例迹TTFF.FF见图4。 反例缩短一B...CDB'...一B...C一B10S. Biallas等人/理论计算机科学电子笔记274（2011）3标准存储状态创建的国家大小[MB]时间[s]同一PC1,502,901179,089,399408.672,123相同散列4,656496,768,47523.74,891身份4,656496,768,47523.75,057表1循环流产标准配备八个AMD Opteron双核处理器和256 GiB RAM。然而，为了获得无偏的结果，仅使用单个处理器4.1基于路径约简的变体第一个案例研究的重点是不同的环路检测标准（cp.节2.3），其确定路径压缩步骤的终止。为了获得真实的结果，要验证的程序必须执行几次循环迭代，理想情况下，迭代的重叠越少越好。 来自我们的基准测试集的一个名为vector的程序满足了这个要求。 这个程序在一个非终止循环中从环境中连续读取输入这些值然后被解释为整数向量并用于不同的典型向量运算。对于每个标准，模型检查器必须生成程序的整个状态空间。这些运行的结果见表1。1.一、参考值没有任何抽象，显示在选项卡中。2、在入口处为矢量。正如预期的那样，“相同pc”准则导致三个与不应用路径缩减的状态空间大小相比，这仍然相当于减少了96.83%。以逐字节的方式比较状态以获得同一性会导致状态空间小得多，这并不奇怪。因此，这个实验的有趣之处在于，确定用于身份检查的e-排序是否关于存储状态的数量，对于该特定程序，在散列冲突检测和状态标识检测之间没有区别。这意味着没有两个不同的状态被映射到相同的哈希值。然而，检查状态标识所需的时间从这些结果来看，我们可以得出结论，检查哈希冲突是运行时和内存消耗问题之间的一个足够的妥协。因此，在下面的案例研究中，我们使用哈希冲突检查作为OPR中的默认标准。4.2与其他抽象技术的比较对于第二组实验，我们使用[MC]S qUARE在不同的抽象层次上生成状态空间：（i）无抽象，（ii）SPR和（iii）OPR。为了进行全面的评估，我们提出了五种不同的微观结构的实验结果，S. Biallas等人/理论计算机科学电子笔记274（2011）311控制器程序 不同运行的结果见表1。二、第一个程序称为灯开关，并基于状态机对电抗性电气开关进行建模。该程序使用两个硬件定时器，但没有中断。模型检查这个非常简单的程序与SPR的结果在减少状态空间大小的73.88%，但它增加了156.69%的状态创建的数量相比之下，OPR将状态空间进一步减少了88.43%。存储在状态空间中的状态的数量越少，在模型检查期间必须重新创建的状态的数量就越少。因此，创建的国家数量增加了约。百分之三百对于这个小程序，这两种技术都没有对内存消耗或运行时间产生明显的影响。在这种情况下，内存占用很大程度上受到用于存储状态空间的哈希表的初始大小的影响。第二个程序叫做plant，它控制一个虚拟的化工厂。它由225行代码组成，比电灯开关（162行）稍长。装置中采用两个中断器和一个定时器. SPR具有显著的效果，将存储的状态数量减少了93.44%。同样，OPR通过减少多达97.54%的状态数量来实现更好的结果。创建状态的数量增加了13.96%，为SPR，22.92%为OPR。因此，与电灯开关的相应数字相比，增加的幅度相当温和。 这意味着模型检查器必须重新访问更少的状态，或者压缩路径的长度更短。使用任何路径缩减技术的内存消耗都下降到哈希表的初始大小附近。在下一个程序中，reentrance，一个16位整数变量在主进程和中断处理程序中同时访问。由于ATmega具有8位架构，因此此类访问是非原子的，从而导致竞争条件。SPR实现的存储状态减少为93.84%。OPR通过将剩余状态的数量减半来进一步减少状态空间，从而减少了96.92%。由于重新访问，SPR的运行时间增加了10.85%，OPR增加了11.94%汽车应用程序被用作第四个程序。该程序称为车窗升降机实现了汽车电动车窗升降机的功能。它基于状态机，状态机根据其当前状态生成输出。为了完成任务，它使用三个中断和一个16位定时器。 状态空间 因为这个没有任何抽象的程序与以前的程序相比是相当大的，由230多万个状态组成。SPR使该值降低了92.2%，而OPR使其降低了94.72%。模型检查所需的运行时间在SPR情况下，存储器消耗减少了89.89%，在OPR情况下减少了92.05%我们的第五个案例研究使用了上述程序向量（cp.第4.1节）。 SPR导致存储的状态数减少了89.76%。OPR的性能超过了三个数量级，减少了99.99%的状态存储数量。这有效地将状态空间所需的内存量从超过11.5 GB（无抽象）减少到23.7 MB（OPR）。SPR导致减少了87.96%，约为1.4 GB，这仍然可以使程序在桌面计算机上进行模型检查所需的时间，12S. Biallas等人/理论计算机科学电子笔记274（2011）3使用SPR仅增加1.55%，而OPR导致增加533%。考虑到使用OPR存储的状态要少得多，这种增加实际上是令人惊讶的低。两种路径简化方法之间的巨大差异的一个解释为了保证在存在程序循环的情况下状态空间生成的终止，SPR必须假设循环中的至少一个位置被中断（cp. [13]）。在我们的实现中，这个位置由循环的头部表示。因此，在每次重新访问磁头的程序计数器位置时，SPR终止当前链并存储状态。另一方面，OPR不必存储在循环的头部（事实上，它不知道程序循环的存在），除非它使用相同的程序计数器方法用于终止检测。 因此，OPR压缩了循环iterations迭代far远more efficiently有效.程序选项使用国存储国创建大小[MB]时间[s]灯开关162条线路没有一4,2686,29621.60.42SPR1,11516,17520.90.79OPR49425,22320.70.88植物225条线路没有一130,524135,94952.282.33SPR8,552154,92122.62.81OPR3,205167,11421.43.03再进入147条线路没有一107,649110,96144.42.60SPR6,628123,00322.02.08OPR3,312124,20721.31.40车窗升降289条线路没有一2,342,5642,589,665633.947.59SPR182,7093,818,06064.157.78OPR123,5854,123,38550.459.49向量930线没有一47,477,79748,419,00311,508.4772SPR4,860,32155,584,4351,385.9784OPR4,656496,768,47523.74,891表2不同路径缩减技术对五种微控制器程序的S. Biallas等人/理论计算机科学电子笔记274（2011）3134.3公式的解释到目前为止，我们在检查公式AG TT时检查了OPR的效果，该公式在任何状态下都是正确的。在本节中，我们将在检查有效性取决于变量的实际公式时评估OPR的效果。由于路径约简需要存储状态时，在过渡的公式，我们预计增加状态空间的大小。对于第一次检查，我们决定使用窗口升降机程序。结果见表1。3 .第三章。如第4.2节所述，该程序对自动电动车窗升降器进行建模，并且基于状态机。 状态机是使用一个名为mode的全局整数变量实现的，在执行过程中的任何时候，该变量都只假定值为0到6。因此，我们的第一个测试是使用公式(1)AG（模式≥0且模式≤ 6），这可以在54.83秒后验证。第二个测试是验证模式假设的状态序列是否满足某个属性。每当传感器报告有物体卡在车窗中时（模式= 5），车窗升降器将完全打开（模式= 6），然后再次允许正常操作（模式= 0），这可以通过公式(2) AG（模式= 5kHzmode = 6）U（mode= 6））。程序窗口升降器包含一个微妙的错误，使该属性无法得到满足。错误是基于两个中断的同时发生这允许模式跳过值6。 [MC]S qUARE正确地发现了此错误并创造了一个由912个状态组成的反例。本案例研究的第二个测试程序是plant，在4.2节中也有详细描述。第一个要验证的属性是，类似于车窗升降器，验证全局变量是否满足某些约束，这些约束可以通过公式(3)AG（tank≥0×tank≤ 4），这也是可以被证实的。第二个属性是确保工厂在紧急情况下的正确行为。 为此，[MC]S qUARE不得不检查公式(4)AG（PORTA= 0x 20）Δ GPORTA = 0x 20）ΔEF（PORTA= 0x 20），这导致了一个在扩展后具有1，643个状态的反例与没有OPR的模型检查相比，所有四个公式的真值是相同的。由于违反了公式（2）和（4），因此模型检查器可以14S. Biallas等人/理论计算机科学电子笔记274（2011）3程序式国存储国创建大小[MB]时间[s]车窗升降（一）226,4523,792,50778.3354.83（二）11,665207,96424.523.64植物（三）3,678167,11421.542.32（四）771,83920.670.6表3状态空间大小提前停止状态空间生成。因此，模型检查的时间和状态空间的大小与其他案例研究不可比较。对于公式（1）的验证，我们的状态空间大小增加了83.24%，而由于重访次数减少，时间略有减少对于公式（3），状态空间大小的增加是可忽略的。5相关工作基于静态分析的模型检查器MUR的路径约简首先由Yorav和Grumberg [18]描述。这种技术在SPIN模型检查器[9]中以类似的方式使用，对其输入语言PROMELA进行静态分析。SPIN使用过程内静态分析（使用内联），与二元代码相比，PROMELA简单得多，因为（1）并发进程之间的通信只能使用区分语句执行，（2）它不包含间接控制语句。后来，Quiros [12]将Yorav和Grumberg的方法应用于虚拟机中使用的字节码语言。这种字节码语言类似于并行while语言。这意味着函数调用是使用内联处理的，通信是在某些程序位置执行的，不支持间接控制。因此，SPR在这一领域是有效的。我们之前的工作[14]通过引入定制的静态分析和修改二进制代码的破坏条件，将这些早期的方法应用于二进制代码验证领域。Behrmann等人[1]为模型检查器UP-PAAL实现了类似的技术，该技术专注于时间自动机。他们的方法类似于我们的SPR实现：他们决定对自动机的控制结构进行静态分析，以获得所谓的边缘覆盖集。使用该集合是为了在状态空间中出现循环的情况下保证终止的国家覆盖集中的边的目标必须被存储，这与SPR中使用的断裂性质完全对应。正如我们已经说明的，在存在长时间运行但终止的循环时，该属性可以证明是SPR的一个显著缺点。我们的贡献，OPR，可以处理这样的循环，而无需在每个S. Biallas等人/理论计算机科学电子笔记274（2011）315反覆项目。Pelanek [11]进行了一项关于非稳态空间缩减技术的调查。他将保持口吃等价的技术归入过渡合并的术语之下。然而，他的调查侧重于高层代表。最近，Yang et al.[17]介绍了动态路径约简用于序列程序的有界然而，即使他们的技术被命名为类似的，其目的是修剪出不可行的执行路径引入的非确定性条件，因此，不能混淆的路径减少在本文中使用的意义。他们的算法使用SMT求解来计算最弱的先决条件和不满足的核心。因此，他们的方法和目标与我们的工作根本不同。6结论性讨论6.1结论本文描述了一种新的动态路径约简技术，并展示了该方法在二进制代码模型检查的具体应用中优于基于静态分析的方法。此外，它还展示了如何使用这种抽象技术生成的反例可以扩展，以减轻其可理解性。在效率方面，OPR方法允许强大的状态空间减少，与静态路径减少技术相比。然而，较小的内存占用可能会导致更高的运行时间。因此，OPR提供了一种允许用运行时间换取内存的技术6.2今后工作Yorav和Grumberg [18]讨论的另一种抽象技术是死变量归约（DVR），其关键思想是重置其值不会在任何后续程序执行中读取的变量。然而，用于二进制代码的DVR特别支持二进制代码中存在的间接读取，其中，使用静态分析通常不能准确地确定源存储器位置[14，6.1节]。因此，评估是否可以使用DVR的在线自适应实现与通过OPR获得的状态空间减少一样显著的状态空间减少将是有趣的[10，15]。确认这项工作得到了DFG超高速信息和通信卓越集群（UMIC）的支持，德国研究基金会授予DFG EXC 89。此外，Sebastian Biallas的工作得到了DFG的支持。J？rgBrauer和D？miniqueGu？cke ll的工作由DFG研究培训组1298反应性和离散性的化学合成提供支持连续系统（AlgoSyn）。 我们感谢Bastian Schlich分享他的想法在本文中描述的想法。16S. Biallas等人/理论计算机科学电子笔记274（2011）3引用[1] Behrmann，G. 、K. G. LAR S ENAR。 Pel'anek，Tostoreorn ottoostore，in：ComputerAideddVerification（CAV 2003），LNCS 2725（2003），pp. 433-445[2] 布朗，M.，E. Clarke和O. Grumberg，Characterizing finite kripke structures in propositionaltemporal logic，Theor. Comput. Sci. 59（1988），pp. 115-131[3] Chaki，S.，A. Groce和O. Strichman，Explaining abstract counterexamples，in：SIGSOFT FSE，2004，pp. 73比82[4] Clarke，E.M.，[5] Clarke，E. M.，O. Grumberg，S. Jha，Y. Lu和H. Veith，模型检验中状态爆炸问题的进展，信息学- 10年前。10 Years Ahead，LNCS 2000（2001），pp. 176-194。[6] Clarke，E. M. 和H. Veith，Counterexamples revisited：Principles，Algorithms，Applications，in：验证：理论与实践，LNCS2772（2004），pp。41比43[7] 库克湾，A. Podelski和A.Rybalchenko，系统代码的终止证明，PLDI（2006），pp.415-426.[8] Heljanko，K.，李国忠，分支时间时序逻辑的模型检验，研究报告A45，赫尔辛基理工大学，数字系统实验室，芬兰埃斯波（1997）。[9] Holzmann，G. J.，The engineering of a model checker：The Gnu i-protocol case study revisited，in ： Theoretical and Practical Aspects of SPIN Model Checking （ SPIN 1999 ） ， LNCS1680（1999），pp. 232- 244。[10] 刘 易 斯 ， M 。 和 M. Jones ， A dead variable analysis for explicit model checking ， in ： PEPM（2006），pp. 48-57.[11]佩拉内克河， On-the-thechystattespacereducti ons，Technicarreport，MasarykUniversityBrno，CzechRepublic（2005）.[12] 去吧G。，“Stat i c Byte- C o d e A naly s is for Stat e Spac e R e duct ion，“M a s t e r sthe s is，R W T H A achen University（2006）.[13] Schlich，B.，“Model Checking of Software for Microcontrollers,” Dissertation, RWTH Aachen University,URLhttp://aib.informatik.rwth-aachen.de/2008/2008-14.pdf[14] Schlich，B.，J. Brauer和S. Kowalewski，应用静态分析减少状态空间到微控制器二进制代码，科学。补偿程序。（2010）出现。[15] Self，J.P.和E. G. Mercer，On-the-Money动态死变量分析，在：SPIN，LNCS4595（2007），pp. 113-130[16] 范格拉贝克河和W.Weijland，BisimulationSemantics中的分支时间和抽象，Journal of the ACM43（1996），pp.555-600[17] 杨志，B. Al-Rawi，K.萨卡拉角Huang，S. Smolka和R. Grosu，软件模型检查，IFM'09：第七届322-336[18] Yorav，K.和O. Grumberg，Static analysis for state-space reductions preserving temporal logics，Formal Methods in System Design25（2004），pp. 67比96
