{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00074106","sets":["1164:1384:6349:6417"]},"path":["6417"],"owner":"11","recid":"74106","title":["情報制御システム記述モデルの検証項目記述とSPINによる確認"],"pubdate":{"attribute_name":"公開日","attribute_value":"2011-03-07"},"_buckets":{"deposit":"a9ea9770-8b19-436d-9e63-141316cdc895"},"_deposit":{"id":"74106","pid":{"type":"depid","value":"74106","revision_id":0},"owners":[11],"status":"published","created_by":11},"item_title":"情報制御システム記述モデルの検証項目記述とSPINによる確認","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"情報制御システム記述モデルの検証項目記述とSPINによる確認"},{"subitem_title":"A Verification Item Description of Information Control System Descriptive Model and Confirmation by SPIN","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"学生セッション：形式手法","subitem_subject_scheme":"Other"}]},"item_type_id":"4","publish_date":"2011-03-07","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"茨城大学"},{"subitem_text_value":"茨城工業高等専門学校"},{"subitem_text_value":"茨城大学"},{"subitem_text_value":"株式会社日立製作所"},{"subitem_text_value":"株式会社日立製作所"},{"subitem_text_value":"株式会社日立製作所"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Ibaraki University","subitem_text_language":"en"},{"subitem_text_value":"Ibaraki National College of Technology","subitem_text_language":"en"},{"subitem_text_value":"Ibaraki University","subitem_text_language":"en"},{"subitem_text_value":"Hitachi Ltd.","subitem_text_language":"en"},{"subitem_text_value":"Hitachi Ltd.","subitem_text_language":"en"},{"subitem_text_value":"Hitachi Ltd.","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"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/74106/files/IPSJ-SE11171010.pdf"},"date":[{"dateType":"Available","dateValue":"2013-03-07"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-SE11171010.pdf","filesize":[{"value":"376.2 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"12"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"adb07930-5b8f-44ee-a33a-e80f3930f219","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2011 by the Information Processing Society of Japan"}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"柳, 翔太"},{"creatorName":"小飼, 敬"},{"creatorName":"上田, 賀一"},{"creatorName":"大久保, 訓"},{"creatorName":"高橋, 勇喜"},{"creatorName":"中野, 利彦"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Shota, Yanagi","creatorNameLang":"en"},{"creatorName":"Kei, Kogai","creatorNameLang":"en"},{"creatorName":"Yoshikazu, Ueda","creatorNameLang":"en"},{"creatorName":"Satoshi, Okubo","creatorNameLang":"en"},{"creatorName":"Yuki, Takahashi","creatorNameLang":"en"},{"creatorName":"Toshihiko, Nakano","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN10112981","subitem_source_identifier_type":"NCID"}]},"item_4_textarea_12":{"attribute_name":"Notice","attribute_value_mlt":[{"subitem_textarea_value":"SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc."}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_18gh","resourcetype":"technical report"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"ソフトウェアの品質を保証するために，ソフトウェア検証を行う必要性が高まっている．そこで，振舞いを網羅的に検証するモデル検査を開発現場に導入することを考える．現在，情報制御システム記述モデルに対してモデル検査を実行する手法が提案されている．しかし，検証すべき事項の記述方法はまとまっていない．そのため，本研究では検証項目記述の定義を行い，検証項目の設計手法について検討した．また，モデル検査で検証する性質を表すLTL(Linear Temporal Logic)式に検証項目を変換するルールを定義した．モデル検査ツールを用いてこれらの有効性を確認した．","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"The necessity to perform software verification is growing in order to guarantee the quality of software. Therefore we think that we introduce a model checking to verify the behavior cyclopaedically into the development field. A technique to execute a model checking for information control system descriptive model is suggested now. However, the description method of the matters which should be verified is not completed. Therefore we defined the verification item description in this study and examined the design technique of the verification item. In addition, we defined a rule to convert a verification item into LTL(Linear Temporal Logic) formula which expressed a property to verify by model checking. We confirmed these effective by using a model checking tool.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"8","bibliographic_titles":[{"bibliographic_title":"研究報告ソフトウェア工学（SE）"}],"bibliographicPageStart":"1","bibliographicIssueDates":{"bibliographicIssueDate":"2011-03-07","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"10","bibliographicVolumeNumber":"2011-SE-171"}]},"relation_version_is_last":true,"weko_creator_id":"11"},"id":74106,"updated":"2025-01-21T21:40:58.668504+00:00","links":{},"created":"2025-01-18T23:31:47.358273+00:00"}