{"updated":"2025-01-23T02:51:12.189541+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00010437","sets":["581:612:624"]},"path":["624"],"owner":"1","recid":"10437","title":["ソフトウェア設計に対するモデル駆動型検証プロセス"],"pubdate":{"attribute_name":"公開日","attribute_value":"2006-01-15"},"_buckets":{"deposit":"e9a87b69-f6ae-49cf-bfb3-29dcd701a100"},"_deposit":{"id":"10437","pid":{"type":"depid","value":"10437","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"ソフトウェア設計に対するモデル駆動型検証プロセス","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"ソフトウェア設計に対するモデル駆動型検証プロセス"},{"subitem_title":"Model Driven Verification Process for Software Design","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"論文","subitem_subject_scheme":"Other"}]},"item_type_id":"2","publish_date":"2006-01-15","item_2_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"株式会社東芝研究開発センター 国立情報学研究所"},{"subitem_text_value":"国立情報学研究所"},{"subitem_text_value":"国立情報学研究所"},{"subitem_text_value":"国立情報学研究所 東京大学"}]},"item_2_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Corporate R&D Center Toshiba Corporation,National Institute of Informatics","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Informatics","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Informatics","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Informatics,The University of Tokyo","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/10437/files/IPSJ-JNL4701019.pdf"},"date":[{"dateType":"Available","dateValue":"2008-01-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-JNL4701019.pdf","filesize":[{"value":"1.1 MB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"8"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"f365f75e-ae59-4896-91eb-d848d910156b","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2006 by the Information Processing Society of Japan"}]},"item_2_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"長野, 伸一"},{"creatorName":"吉岡, 信和"},{"creatorName":"田原, 康之"},{"creatorName":"本位田真一"}],"nameIdentifiers":[{}]}]},"item_2_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Shinichi, Nagano","creatorNameLang":"en"},{"creatorName":"Nobukazu, Yoshioka","creatorNameLang":"en"},{"creatorName":"Yasuyuki, Tahara","creatorNameLang":"en"},{"creatorName":"Shinichi, Honiden","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_2_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN00116647","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_2_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7764","subitem_source_identifier_type":"ISSN"}]},"item_2_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"本研究では，新しいソフトウェアプロセスの1 つとしてモデル駆動型検証プロセスを提案する．一般に，設計検証とは，実践的ノウハウや経験を必要とする，習得のハードルが非常に高い作業である．しかし，これまで検証プロセスは，それらのノウハウや経験に沿って体系化されていないため，経験の浅いソフトウェア開発者にとって，検証は依然として困難な作業となっている．提案プロセスは，この課題に対する解決を目的とするものである．本研究では，検証プロセスを，中間成果物である検証モデルに対する変換手続きととらえ，そのうえで検証に必要な具体的作業の順序と内容を体系的に定義する．提案プロセスは次の2 つの特長を持つ．第1 に，検証作業に有効な実用的ノウハウの利用方法を明確化している．第2 に，検証モデル間の変換手続きの逆像が，設計誤り発見のためのデバッグプロセスの定義になっている．さらに，3 つのモデル検査ツール，SPIN，Cadence SMV，LTSAのそれぞれを利用した3 つの検証プロセスのインスタンスを示し，各プロセスをネットワーク家電の制御ソフトウェア設計に適用した事例を示す．その適用結果に基づいて，提案プロセスの特長と有効性に対する評価について述べる．","subitem_description_type":"Other"}]},"item_2_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_2_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"208","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌"}],"bibliographicPageStart":"193","bibliographicIssueDates":{"bibliographicIssueDate":"2006-01-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"1","bibliographicVolumeNumber":"47"}]},"relation_version_is_last":true,"item_2_alternative_title_2":{"attribute_name":"その他タイトル","attribute_value_mlt":[{"subitem_alternative_title":"ソフトウェア分析・設計技法"}]},"weko_creator_id":"1"},"created":"2025-01-18T22:45:20.866720+00:00","id":10437,"links":{}}