文献

J-GLOBAL ID：201102230829732918   整理番号：11A0858867

有界モデル検査法を用いたモジュラー検証のテストケース生成による補完

Modular Verification using Bounded Model Checking technique with Test Case Generation

著者 (4件)： 橋本祐介 (総合研究大学院大) ,  橋本祐介 (NEC サービスプラットフォーム研) ,  中島震 (総合研究大学院大) ,  中島震 (国立情報学研)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 110  号： 458(SS2010 53-78)  ページ： 91-96  発行年： 2011年02月28日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 有界モデル検査法では,プログラムを有限状態遷移システムに変換する際に近似を導入する。近似は誤警告や不具合の見過しという問題を起こす。検査できなかったパスは別の方法で調べる必要がある。本研究では,ソフトウェアモデル検査をテストで補完するために,近似の検知とテストケース生成の方式を提案し,構造カバレッジ基準に則った提案手法の有効性を実験により示す。(著者抄録)

シソーラス用語： 限界 ,  モデル検査 ,  *モジュール ,  *検証 ,  補完 ,  *ソフトウェア ,  プログラム検証 ,  近似法
準シソーラス用語： カバレッジ【プログラム検証】 ,  *テストケース ,  近似 ,  有界

分類 (1件)： 計算機システム開発  (JD02010R)

引用文献 (13件)：

• CLARKE, E. M. Model Checking. 1999
• CLARKE, E. M. A tool for checking ansi-c programs. Proc. TACAS'04. 2004, 168-176
• DICK, J. Automating the generation and sequencing of test cases from model-based specifications. Proc. FME'93. 1993, 268-284
• LIU, S. Integrating specification-based review and testing for detecting errors in programs. Proc. ICFEM'07. 2007, 136-150
• MEYER, B. Applying design by contract. IEEE Computer. 1992, 25, 10, 40-51

タイトルに関連する用語 (5件)： 有界 ,  モデル検査 ,  検証 ,  テストケース生成 ,  補完