ソフトウェア設計に対するモデル駆動型検証プロセス

情報処理学会 Web Site 被引用文献2件 参考文献22件

書誌事項

タイトル別名
  • ソフトウェア セッケイ ニ タイスル モデル クドウガタ ケンショウ プロセス
  • Model Driven Verification Process for Software Design
  • ソフトウェア分析・設計技法

この論文をさがす

抄録

本研究では，新しいソフトウェアプロセスの1 つとしてモデル駆動型検証プロセスを提案する．一般に，設計検証とは，実践的ノウハウや経験を必要とする，習得のハードルが非常に高い作業である．しかし，これまで検証プロセスは，それらのノウハウや経験に沿って体系化されていないため，経験の浅いソフトウェア開発者にとって，検証は依然として困難な作業となっている．提案プロセスは，この課題に対する解決を目的とするものである．本研究では，検証プロセスを，中間成果物である検証モデルに対する変換手続きととらえ，そのうえで検証に必要な具体的作業の順序と内容を体系的に定義する．提案プロセスは次の2 つの特長を持つ．第1 に，検証作業に有効な実用的ノウハウの利用方法を明確化している．第2 に，検証モデル間の変換手続きの逆像が，設計誤り発見のためのデバッグプロセスの定義になっている．さらに，3 つのモデル検査ツール，SPIN，Cadence SMV，LTSAのそれぞれを利用した3 つの検証プロセスのインスタンスを示し，各プロセスをネットワーク家電の制御ソフトウェア設計に適用した事例を示す．その適用結果に基づいて，提案プロセスの特長と有効性に対する評価について述べる．

This paper proposes a model-driven verification process that is yet another software process. Generally, verification is a very difficult task that calls for practical tips and experiences. However, no verification processes have been established systematically along with the tips and experiences. As a result, it is still difficult for software developers without enough experiences to begin on the verification task. The proposed process is a solution to this issue. It is defined as transformation procedures of intermediate products yielded during verification, systematizing the order and the contents of the activities needed for verification. The process has the following two advantages. First, it makes clear how to use the practical tips of verification. Second, the inverse images of the model transformation procedures result in the definition of debugging process for detecting design faults. We also illustrate a case study of application of three verification process instances using three model checkers, SPIN, Cadence SMV, and LTSA, respectively, to digital appliance control software. With the results of the applications, we evaluate the advantages and the effects of our proposed process.

収録刊行物

被引用文献 (2)*注記

もっと見る

参考文献 (22)*注記

もっと見る

キーワード

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

問題の指摘

ページトップへ