文献

J-GLOBAL ID：201102226800542519   整理番号：11A1375668

有界モデル検査法を用いたCプログラムのモジュラー検証

Modular Verification of C Programs with Bounded Model Checking Method

著者 (4件)： 橋本祐介 (総合研究大学院大) ,  橋本祐介 (NEC サービスプラットフォーム研) ,  中島震 (国立情報学研) ,  中島震 (総合研究大学院大)
資料名： 情報処理学会論文誌ジャーナル(CD-ROM)  (情報処理学会論文誌 論文誌ジャーナル(CD-ROM))
巻： 52  号： 8  ページ： 2422-2430  発行年： 2011年08月15日 
JST資料番号： Z0778B  ISSN： 1882-7837  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ソフトウェアモデル検査はプログラムの信頼性向上の有望な手段である。本研究では,Cプログラムを対象としたSATに基づく有界モデル検査法にDesign by Contract(DbC)の考え方を明示的に取り入れる。DbCに基づくモジュラー検証を実現することにより,モデル検査が直面するスケーラビリティの問題を解消する。さらに,関数ポインタを用いたCプログラムへのDbCの導入手法を提案し,MINIXソースコードを対象とした実験により誤検出の削減や不具合の検出の観点から効果を示した。(著者抄録)

シソーラス用語： *モデル検査 ,  *充足可能性問題 ,  性質 ,  スケーラビリティ【計算機】 ,  計算機コード ,  C言語 ,  誤り検出 ,  *デバッギング ,  計算機プログラム
準シソーラス用語： Cプログラム ,  ソースコード ,  モジュラ性

分類 (3件)： 計算理論  (JB02000A) ,  論理代数  (JB03000H) ,  計算機システム開発  (JD02010R)

引用文献 (22件)：

• 1) Ball, T. and Rajamani, S.K.: The SLAM Project: Debugging System Software via Static Analysis, Proc. POPL 2002, pp.1-3 (2002).
• 2) Baudin, P., Filliatre, J.-C., Marche, C., Monate, B., Moy, Y. and Prevosto, V.: ACSL: ANSI/ISO C Specification Language (2008).
• 3) Biere, A., Cimatti, A., Clarke, E. and Zhu, Y.: Symbolic Model Checking without BDDs, Proc. TACAS 1999, pp.193-207 (1999).
• 4) Clarke, E.M., Grumberg, O. and Peled, D.A.: Model Checking, The MIT Press (1999).
• 5) Clarke, E.M., Kroening, D. and Lerda, F.: A Tool for Checking ANSI-C Programs, Proc. TACAS'04, pp.168-176 (2004).

タイトルに関連する用語 (3件)： 有界 ,  モデル検査 ,  検証