文献

J-GLOBAL ID：201002269003118012   整理番号：10A0035131

ソフトウェアのモデル検査

Software Model Checking

著者 (2件)： JHALA Ranjit (Univ. California, San Diego) ,  MAJUMDAR Rupak (Univ. California, Los Angeles)
資料名： ACM Computing Surveys  (ACM Computing Surveys)
巻： 41  号： 4  ページ： 21.1-21.54  発行年： 2009年10月 
JST資料番号： E0003B  ISSN： 0360-0300  資料種別： 逐次刊行物 (A)
記事区分： 文献レビュー  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： ソフトウェアのモデル検査は,プログラムのアルゴリズムを解析し,その実行特性を証明する。Turingの決定不能性定理は,健全かつ完全なアルゴリズム解の可能性を否定し,正しさ問題は計算困難に留まっている。しかし一般問題が決定不能としても,問題の特定事例が扱えないとは限らない。本論文はまず,モデル検査において状態を表現する2つの主な方法として,総当たり法と記号的方法を具体的に示した。次に状態空間を精度の犠牲で縮小する抽象技法と,抽象解析の精度を向上する自動化技法を示した。この結果,プログラムの状態は,一部は総当たり形式で,一部は記号的に表現され,両者は種々の抽象により組合せされる。基本手法の拡張技法を示した後,モデル検査技法と関連する動的検査技法および静的型システム技法のソフトウェア品質における関連性を考察した。現行ツールの限界と,将来の課題を示した。

シソーラス用語： *モデル検査 ,  ソフトウェア工学 ,  計算機アルゴリズム ,  計算機プログラム ,  プログラム実行 ,  ソフトウェア仕様 ,  非決定性 ,  プログラムの正しさ ,  空間 ,  次元縮小 ,  抽象 ,  自動化 ,  記号処理 ,  プログラム検査 ,  仕様記述 ,  支援プログラム ,  文献展望 ,  精度 ,  型システム ,  解析精度 ,  改変
準シソーラス用語： 状態空間

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

タイトルに関連する用語 (2件)： ソフトウェア ,  モデル検査