模型检测中状态爆炸问题研究综述

Survey of State Explosion Problem in Model Checking

模型检测已成为保证软件系统正确性和可靠性的重要手段,但随着软件功能日益强大,其规模和复杂度也越来越大,在模型检测过程中容易产生状态爆炸问题。如何解决模型检测中的状态爆炸,已成为工业界和理论界无法回避的重要课题。系统地综述模型检测领域解决状态爆炸问题的关键技术和主要方法,并提出该领域的最新研究进展与方向。

Model checking has become an important approach to ensure the correctness and reliability software systems. However, with the increasingly powerful software functionality, system scale and complexity are also growing. Then it is easy to produce state explosion problem in model checking process. How to solve the state explosion in model checking has become an important issue that can not be avoided by the industry and theorists. In this paper, we overviewed the key technology and main methods of solving state explosion problem, and proposed the latest research progress and direction in this field of model checking.