分而治之的方法导致大规模系统的模型检查

导读 模型检查是过去几十年来最成功的计算机科学成就之一。这就是EdmundM.Clarke、E.AllenEmerson和JosephSifakis因其在将模型检查开发为高效验...

模型检查是过去几十年来最成功的计算机科学成就之一。这就是EdmundM.Clarke、E.AllenEmerson和JosephSifakis因其在将模型检查开发为高效验证技术方面所发挥的作用而荣获2007年AM图灵奖的原因。

(资料图片)

模型检查已被广泛采用，特别是在硬件行业，因为它可以系统地验证系统是否满足所需的属性。然而，模型检查仍然存在一些问题需要解决，其中之一就是臭名昭著的状态爆炸。人们已经设计出了许多减轻状态爆炸的技术，例如偏序约简和抽象。

尽管有这些现有技术，但它们可能不足以应对状态爆炸。另一个目标是提高模型检查的运行性能。解决这个问题的一种有前景的方法是并行化模型检查，这可以充分利用多核架构。

由KazuhiroOgata教授领导的日本先进科学技术研究所(JAIST)的一个研究小组提出了一种“分而治之”的方法来进行模型检查，称为DCA2L2MC。正如其名称所示，DCA2L2MC致力于引导属性，它非正式地描述了每当某件事成为现实时，其他事情最终也会成为现实。

Chandy和Misra设计了一种称为UNITY的时间逻辑，其中导数时间连接词发挥着重要作用，并且他们证明了许多基本的系统需求可以表示为导数属性。因此，关注导向属性是有益的。有关DCA2L2MC的详细信息已发表在ACMTransactionsonSoftwareEngineeringandMethodology的一篇文章中。

DCA2L2MC的核心思想是将一个原始的模型检查问题分层划分为多个较小的模型检查问题，并独立处理每个较小的模型检查问题。具体来说，DCA2L2MC将每个初始状态的可达状态空间划分为L+1层，其中L是正自然数，生成多个子状态空间。然后对每个子状态空间而不是原始的可达状态空间进行模型检查实验。

如果每个子状态空间比原始可达状态空间小得多，则即使由于状态空间爆炸问题而无法直接对原始可达状态空间进行引导模型检​​查，也可以进行引导模型检​​查。这是使用DCA2L2MC缓解模型检查中状态空间爆炸问题的关键。

此外，由于分而治之方法的性质，每个较小的模型检查问题都可以独立解决。特别是，我们划分的最后一层中较小的模型检查问题是完全独立的。这是DCA2L2MC利用并行化提高模型检查运行性能的关键。

从理论角度来看，研究人员证明了一个保证DCA2L2MC正确性的定理，表明多重模型检查问题与原始的引导模型检​​查问题是等价的。在实践方面，他们用Maude开发了DCA2L2MC的支持工具，Maude是一种基于重写逻辑的高性能规范/编程语言。该支持工具提供了根据需要以顺序和并行模式运行的灵活性。

已经进行了几个案例研究来证明该方法在模型检查导向属性方面的有效性和效率。此外，他们还证明，与SPIN和LTSMin等现有模型检查器相比，DCA2L2MC作为一种在大型系统中检查模型属性的技术具有重大前景。

为了充分利用DCA2L2MC，研究人员提出了两种优化技术：一种是使用新的模型检查器在模型检查中一次找到所有反例，另一种是使用分析工具为DAC2L2MC找到良好的层配置。第一种技术在DCA2L2MC中高效生成所有反例方面发挥着至关重要的作用，显着提高了其运行性能。第二种技术对于找到优化DCA2L2MC运行性能的良好层配置至关重要。通过利用这两种优化技术，DCA2L2MC的验证变得更加有效和高效。

最后，DCA2LCMC可以集成到现有的模型检查器中，使它们能够在更大的系统上执行模型检查。研究人员希望现有的几个模型检查器能够采用DCA2LCMC作为处理引导属性的有效且高效的技术。此外，研究人员和工程师可以轻松地采用该技术和工具来对具有引导属性的系统进行验证。

免责声明：本文由用户上传，如有侵权请联系删除！