非同期並行システムに対するSATに基づくモデル検査 A SAT-based Model Checking Method for Asynchronous Concurrent Systems

新しい自動検証手法として,論理式の充足可能性判定(SAT)を利用した限定モデル検査(Bounded Model Checking)と呼ばれる手法が注目されている.しかし従来の限定モデル検査手法には,非同期的に動作する並行システムを対象とした場合,判定する論理式が複雑になるため検証時間が非常に大きくなるという問題があった.そこで本論文では,非同期並行システムのモデルであるペトリネットを対象として,新しい論理式の生成手法を提案する.提案手法を用いてシステムの動作を簡潔な論理式で表現することによって,実用的な時間での検証が可能となる.実際の並行プログラムをモデル化したペトリネットの例を用いて提案法の有効性を実験的に示す.

Bounded model checking has received recent attention as an efficient verification method. The basic idea of this method is to reduce the model checking problem to the propositional satisfiability (SAT) decision problem. For asynchronous systems, however, this method does not work well because the resulting propositional formulastend to become very large for such systems. In this paper, we take 1-bounded Petri nets as a plausible model of asynchronous systems and propose an alternative encoding method for them. This method is simple but can generate very succinct formulas, thus resulting in reduced verification times.