WEKO3
-
RootNode
アイテム
ソフトウェア設計に対するモデル駆動型検証プロセス
https://ipsj.ixsq.nii.ac.jp/records/10437
https://ipsj.ixsq.nii.ac.jp/records/104371051b01f-3e41-4b10-a284-5dc4203c59b4
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-JNL4701019.pdf (1.1 MB)
|
Copyright (c) 2006 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Journal(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2006-01-15 | |||||||
| タイトル | ||||||||
| タイトル | ソフトウェア設計に対するモデル駆動型検証プロセス | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Model Driven Verification Process for Software Design | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| その他タイトル | ||||||||
| その他のタイトル | ソフトウェア分析・設計技法 | |||||||
| 著者所属 | ||||||||
| 株式会社東芝研究開発センター 国立情報学研究所 | ||||||||
| 著者所属 | ||||||||
| 国立情報学研究所 | ||||||||
| 著者所属 | ||||||||
| 国立情報学研究所 | ||||||||
| 著者所属 | ||||||||
| 国立情報学研究所 東京大学 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Corporate R&D Center Toshiba Corporation,National Institute of Informatics | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| National Institute of Informatics | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| National Institute of Informatics | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| National Institute of Informatics,The University of Tokyo | ||||||||
| 著者名 |
長野, 伸一
吉岡, 信和
田原, 康之
本位田真一
× 長野, 伸一 吉岡, 信和 田原, 康之 本位田真一
|
|||||||
| 著者名(英) |
Shinichi, Nagano
Nobukazu, Yoshioka
Yasuyuki, Tahara
Shinichi, Honiden
× Shinichi, Nagano Nobukazu, Yoshioka Yasuyuki, Tahara Shinichi, Honiden
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本研究では，新しいソフトウェアプロセスの1 つとしてモデル駆動型検証プロセスを提案する．一般に，設計検証とは，実践的ノウハウや経験を必要とする，習得のハードルが非常に高い作業である．しかし，これまで検証プロセスは，それらのノウハウや経験に沿って体系化されていないため，経験の浅いソフトウェア開発者にとって，検証は依然として困難な作業となっている．提案プロセスは，この課題に対する解決を目的とするものである．本研究では，検証プロセスを，中間成果物である検証モデルに対する変換手続きととらえ，そのうえで検証に必要な具体的作業の順序と内容を体系的に定義する．提案プロセスは次の2 つの特長を持つ．第1 に，検証作業に有効な実用的ノウハウの利用方法を明確化している．第2 に，検証モデル間の変換手続きの逆像が，設計誤り発見のためのデバッグプロセスの定義になっている．さらに，3 つのモデル検査ツール，SPIN，Cadence SMV，LTSAのそれぞれを利用した3 つの検証プロセスのインスタンスを示し，各プロセスをネットワーク家電の制御ソフトウェア設計に適用した事例を示す．その適用結果に基づいて，提案プロセスの特長と有効性に対する評価について述べる． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN00116647 | |||||||
| 書誌情報 |
情報処理学会論文誌 巻 47, 号 1, p. 193-208, 発行日 2006-01-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7764 | |||||||
