MISC

2019年3月

証明支援系Coqを用いた有界モデル検査アルゴリズムの検証

情報処理学会論文誌プログラミング(PRO)
  • 藤井 采人
  • ,
  • 石井 大輔

12
3
開始ページ
1
終了ページ
1
記述言語
日本語
掲載種別
研究発表ペーパー・要旨(全国大会,その他学術会議)

有界モデル検査(bounded model checking,BMC)は,システム(状態遷移系)と性質を述語論理式にエンコードし,その充足性をSAT/SMTソルバーで判定することにより,システムの安全性を示したり,不具合を見つけたりするための方法である.さまざまなBMCアルゴリズム(BMC法)が提案されているが,それぞれの方法は,実行パスのunrolling,実行パスに関する帰納法,状態の抽象表現など煩雑な考察に基づいて設計されている.BMC法の設計や実装にあたっては,背景の考察を理解して正確に行わなければ,検査器の信頼性が損なわれてしまう.そこで本研究では,高信頼なBMCツールの実現を目標に,BMC法および背景となる考察を証明支援系を用いて記述・検証し,さらに前記BMC法の記述をそのまま用いて検査を実施可能にする.具体的には,証明支援系Coq上にSheeranらが提案したBMC法を実装し,その健全性を証明し,プラグインされたSMTソルバーを利用して検査を実施可能にした.本研究の貢献は,(1) Sheeranらが提案した複数のBMC法とその健全性の証明をCoqで記述・形式化するとともに,一般的なBMC法へ流用可能な関数や定理を同定・整備したこと,(2)システム,性質,BMC法,その健全性の証明,SMTソルバーの入出力等をCoq上で記述し,検査対象システムの記述,システムの検査,BMC法の正しさの検証といった作業を統合したこと,の2点である.

リンク情報
CiNii Articles
http://ci.nii.ac.jp/naid/170000180465
CiNii Resolver ID
http://ci.nii.ac.jp/nrid/9000404481917