講演抄録/キーワード |
講演名 |
2011-03-08 09:00
有界モデル検査法を用いたモジュラー検証のテストケース生成による補完 ○橋本祐介(総研大/NEC)・中島 震(NII/総研大) SS2010-68 |
抄録 |
(和) |
有界モデル検査法では,プログラムを有限状態遷移システムに変換する際に近似を導入する.近似は誤警告や不具合の見過しという問題を起こす.検査できなかったパスは別の方法で調べる必要がある.本研究では,ソフトウェアモデル検査をテストで補完するために,近似の検知とテストケース生成の方式を提案し,構造カバレッジ基準に則った提案手法の有効性を実験により示す. |
(英) |
In bounded model checking technique, some approximation is introduced during the translation from a program to a finite state transition system. The approximation causes problems such as spurious alarms and the oversight of defects in the program. We propose an approach to the augmentation of software model checking with test case generation based on specifications. The result of our experiment shows the effectiveness of the proposed approach from the viewpoint of the structural coverage criteria. |
キーワード |
(和) |
有界モデル検査 / 近似 / テストケース生成 / カバレッジ / / / / |
(英) |
bounded model checking / approximation / test case generation / coverage / / / / |
文献情報 |
信学技報, vol. 110, no. 458, SS2010-68, pp. 91-96, 2011年3月. |
資料番号 |
SS2010-68 |
発行日 |
2011-02-28 (SS) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2010-68 |