文献

J-GLOBAL ID：200902279827147300   整理番号：09A0033366

ソフトウェア設計に対するモデル検査のための検証パターン

Verification Patterns for Model Checking Software Design

著者 (2件)： 金井勇人 (北陸先端科学技術大学院大) ,  岸知二 (北陸先端科学技術大学院大)
資料名： 情報処理学会論文誌ジャーナル(CD-ROM)  (情報処理学会論文誌 論文誌ジャーナル(CD-ROM))
巻： 49  号： 10  ページ： 3493-3507  発行年： 2008年10月15日 
JST資料番号： Z0778B  ISSN： 1882-7837  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本稿ではモデル検査技術を用いたソフトウェア設計検証のための検証パターンを提案する。ソフトウェア設計検証においては,時相論理式等が必要だが,その記述はソフトウェア技術者にとって扱いにくい作業である。本研究では,ソフトウェアの構造によって確認したい典型的な性質があり,またその確認方法にはいくつかの定石があることに注目し,ソフトウェア構造と性質とを合わせて体系づけたパターンを提案する。また,このパターンの例題を用いた評価も合わせて報告する。(著者抄録)

シソーラス用語： *モデル検査 ,  *ソフトウェア設計 ,  プログラム構造 ,  型 ,  システム評価 ,  仕様記述言語 ,  時間論理
準シソーラス用語： パターン ,  検証パターン

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

引用文献 (14件)：

• http://spinroot.com/spin
• Holzmann, G. J.: The SPIN Model Checker, Addison-Wsley (2004).
• Clarke, E., Grumberg, O. and Peled, D.: Model Checking, MIT (1999).
• 岸 知二, 青木利晃, 中島 震, 野田夏子, 片山卓也: プロジェクト紹介: 高信頼組込み用オブジェクト指向設計技術, 情報処理学会ソフトウェア工学研究会, SE146-7, pp. 41-46(2004).
• Dwyer, M. B., Avrunin, G. S. and James, C.: Patterns in Property Specifications for Finite-state Verification, The 21st International Conference on Software Engineering (May 1999).

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