充足可能性判定を利用したモデル検査 Model Checking that Uses Satisfiability Solving

この論文にアクセスする

この論文をさがす

著者

抄録

本解説記事では,論理式の充足可能性判定を利用したモデル検査について説明する.モデル検査とは,アルゴリズムやシステムの設計に対して,その状態空間を探索することで,与えられた性質が満たされるかどうかを判定する自動検証手法である.近年高速化が著しい充足可能性判定ツール(SATソルバやSMTソルバ)を用いることで,高速な検証が実現できる.本稿では,まずモデル検査や充足可能性判定について概説した後,プログラムのソースコードをモデル検査する手法について説明する.次に,より一般的なシステム記述を検証対象とした場合について,有界モデル検査と呼ばれる手法を紹介する.これは,初期状態からの有限の決められた回数の遷移による動作について検証を行う手法である.更に,この制約を取り除き,システムの全動作を対象とした検証を実現する手法について説明する.

This article describes model checking techniques that use satisfiability solving. Model checking is an automatic verification method which determines whether a given property holds or not by exploring the state space of a system. Satisfiability solving-based model checking can enjoy the recent rapid performance improvement of SAT or SMT solvers. In this article we first describe the basics of model checking and of satisfiability solving. Then we explain how program's source code can be model checked using satisfiability solving. Next we focus on a more general class of systems and describe bounded model checking for it. This technique is bounded in the sense that the state search is limited to the space reachable within a fixed number of transitions. We also show how this limitation can be removed to allow verifying the whole behavior of the system.

収録刊行物

  • コンピュータソフトウェア

    コンピュータソフトウェア 29(1), 19-29, 2012-01-26

    Japan Society for Software Science and Technology

参考文献:  37件中 1-37件 を表示

各種コード

  • NII論文ID(NAID)
    10030021137
  • NII書誌ID(NCID)
    AN10075819
  • 本文言語コード
    JPN
  • 資料種別
    REV
  • ISSN
    02896540
  • NDL 記事登録ID
    023515853
  • NDL 請求記号
    Z14-1033
  • データ提供元
    CJP書誌  NDL  J-STAGE 
ページトップへ