ソフトウェアモデル検査とテストケース生成の統合

情報処理学会 Web Site

書誌事項

タイトル別名
  • ソフトウェア モデル ケンサ ト テストケース セイセイ ノ トウゴウ
  • Combining Software Model Checking and Test Case Generation

この論文をさがす

抄録

有界モデル検査はプログラムの信頼性を向上させる有力な手段である．しかし，プログラムを有限状態遷移系へ変換する過程で，広い意味での近似を導入することから，誤警告や不具合の見過しを起こすという問題がある．本研究では，この問題に対して有界モデル検査をテストケース生成で補うツールを提案する．とくに，不具合の見過しの原因となる過小近似の場合について，有界モデル検査とテスト実行に共通のカバレッジ基準の下で，近似導入の有無を自動検知する方式を提案する．MINIXのソースコードを対象とした実験により，有界モデル検査とテスト実行とをあわせて，カバレッジ基準を満たす検査が行えることを示した．

Bounded Model Checking (BMC) is a promising approach to achieving high quality of programs. In BMC, programs are translated into finite-state transition systems to introduce some approximation. It may result in false alarms or missing of errors. We propose a tool to augment BMC with test case generation. It includes an automated way of detecting under-approximation and a specification-based test case generation method, both of which employs a common coverage criteria. We also demonstrate the effectiveness of our approach by applying it to checking of MINIX source codes.

収録刊行物

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ