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

書誌事項

タイトル別名
  • ソフトウェア セッケイ ニ タイスル モデル ケンサ ノ タメ ノ ケンショウ パターン
  • Verification Patterns for Model Checking Software Design
  • 検証/テストとデバッグ

この論文をさがす

抄録

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

In this paper, we propose verification patterns for software design verification utilizing model checking techniques. In verifying software design model, we have to develop target model and define properties depending on the target model. As, typical software structures have their own listing of important properties, it is useful to define each verification pattern as a set of software structure, its important properties, and verification techniques. We introduce verification patterns based on the idea, and demonstrate their usefulness based on a case study.

収録刊行物

参考文献 (6)*注記

もっと見る

詳細情報 詳細情報について

問題の指摘

ページトップへ