2024-03-29T07:39:07Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000775552023-11-14T00:51:14Z06164:06165:06522:06534
ソフトウェアモデル検査とテストケース生成の統合ツールチェインA Tool Chain to Combine Software Model Checking and Test Case Generationjpn形式手法http://id.nii.ac.jp/1001/00077555/Conference Paperhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=77555&item_no=1&attribute_id=1&file_no=1Copyright (c) 2011 by the Information Processing Society of Japan総合研究大学院大学/日本電気株式会社国立情報学研究所/総合研究大学院大学橋本, 祐介中島, 震有界モデル検査はプログラムの信頼性を向上する有力な手段である.しかし,プログラムを有限状態遷移システムへ変換する過程で,広い意味での近似を導入することから,誤警告や不具合の見過しを起こすという問題がある.本研究では,この問題に対して有界モデル検査をプログラムテスティングで補うツールチェインを提案する.特に,不具合の見過しの原因となる過小近似の場合について,有界モデル検査とテスティングに共通のカバレッジ基準の下で,近似導入の有無を自動検知する方式を提案する.MINIX のソースコードを対象とした実験により,有界モデル検査とテスティングとを合せて,カバレッジ基準を満たす検査が行えることを示した.Bounded Model Checking (BMC) is a promising appraoch to achieving high quality of programs. In BMC, programs are translated into finite-state transi-tion systems to introduce some approximation. It may result in spurious alarms or missing of errors. We propose a set of tools to augment BMC with program testing. It includes an automated way of detecting under-approximation and a specification-based test generation method, both of which employs a common coverage criteria. We also demonstrate effectiveness of our approach by applying it to checking of MINIX source codes.ソフトウェアエンジニアリングシンポジウム2011論文集2011182011-09-062011-09-12