{"created":"2023-05-15T08:43:56.845349+00:00","id":9105,"links":{},"metadata":{"_buckets":{"deposit":"e3840da1-f186-454b-bc20-0fc4029366bb"},"_deposit":{"created_by":13,"id":"9105","owners":[13],"pid":{"revision_id":0,"type":"depid","value":"9105"},"status":"published"},"_oai":{"id":"oai:uec.repo.nii.ac.jp:00009105","sets":["6"]},"author_link":["24818","24819","24820","24821"],"control_number":"9105","item_10001_biblio_info_7":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2005-02-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"2","bibliographicPageEnd":"469","bibliographicPageStart":"459","bibliographicVolumeNumber":"46","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌","bibliographic_titleLang":"ja"}]}]},"item_10001_description_5":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"インターネットやイントラネットなどの広域開放型ネットワークが普及するにつれて，Webサービスやエージェントといった，開放型ネットワーク環境を有効に活用するための分散システム開発技術が急速に進展している．一方，その急速な発展のため，これらの技術を用いて実際の開発を行う際に，このような大規模かつ複雑なシステムが，機能やセキュリティなどに関し，要求仕様を満足しているかどうかを確認することが困難になってきている．従来このような問題を解決するための最も有効な技術の1 つとして，モデル検査手法などの形式的検証技術があるが，実適用は現在でも容易ではない．本論文では，分散システム開発において，視覚的な支援により，モデル検査の適用を容易にする手法を提案する．本手法では，開発ツールIPEditorで作成した視覚的モデルに対し，その形式的表現を与え，そのモデルからモデル検査ツールSPINが検証の対象とするPromelaプログラムの一部を自動的に生成する．これにより，開発者は記述が困難なPromelaプログラムの全体を直接記述しなくても，IPEditorにより理解が容易な視覚的モデルを作成することにより，SPINツールを利用したモデル検査を用意に実施することができる．","subitem_description_type":"Abstract"},{"subitem_description":"As wide-area open networks like the Internet and intranets grow larger, various technology of distributed system development is rapidly emerging such as the Web service technology and the agent technology. On the other hand, the growth is so rapid that people are reporting a number of difficulties in actually operating practical systems such as management of complexity, poor flexibility to cope with frequent changes of requirements and environments, and security issues. Although the vendors are considering such difficulties, one of the most effective techniques is still in an early stage of research, that is, formal verification including model checking. Application of formal verification techniques is thought of as difficult because it is not easy to create models to verify. In this paper, we propose a method that visually supports model checking and development of distributed systems. Our technique realizes integration of visual modeling and model checking by providing formal representations of the visual models and a procedure of generation of a part of Promela programs that are formal models for the model checking tool SPIN. We can create the visual models using IPEditor, a development support tool for multi-agent applications originally and also applicable to other technologies including Web services. Thus the developer do not have to describe the entire Promela programs directly and therefore easily use SPIN in system development. We demonstrate the advantage of our method with an example of mutual exclusion.","subitem_description_type":"Abstract"}]},"item_10001_publisher_8":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会"}]},"item_10001_relation_17":{"attribute_name":"関連サイト","attribute_value_mlt":[{"subitem_relation_type_id":{"subitem_relation_type_id_text":"http://id.nii.ac.jp/1001/00010704/","subitem_relation_type_select":"URI"}}]},"item_10001_rights_15":{"attribute_name":"権利","attribute_value_mlt":[{"subitem_rights":"(c) 2005 Information Processing Society of Japan. 本著作物の著作権は情報処理学会に帰属します。本著作物は著作権者である情報処理学会の許可のもとに掲載するものです。ご利用に当たっては「著作権法」ならびに「情報処理学会倫理綱領」に従うことをお願いいたします。"}]},"item_10001_source_id_9":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"18827764","subitem_source_identifier_type":"ISSN"}]},"item_10001_version_type_20":{"attribute_name":"著者版フラグ","attribute_value_mlt":[{"subitem_version_resource":"http://purl.org/coar/version/c_970fb48d4fbd8a85","subitem_version_type":"VoR"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"田原, 康之","creatorNameLang":"ja"},{"creatorName":"タハラ, ヤスユキ","creatorNameLang":"ja-Kana"},{"creatorName":"Tahara, Yasuyuki","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"吉岡, 信和","creatorNameLang":"ja"},{"creatorName":"ヨシオカ, ノブカズ","creatorNameLang":"ja-Kana"},{"creatorName":"Yoshioka, Nobukazu","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"大須賀, 昭彦","creatorNameLang":"ja"},{"creatorName":"オオスガ, アキヒコ","creatorNameLang":"ja-Kana"},{"creatorName":"Ohsuga, Akihiko","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"本位田, 真一","creatorNameLang":"ja"},{"creatorName":"ホンイデン, シンイチ","creatorNameLang":"ja-Kana"},{"creatorName":"Honiden, Shinichi","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2019-04-09"}],"displaytype":"detail","filename":"IPSJ-JNL4602014.pdf","filesize":[{"value":"262.4 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"IPSJ-JNL4602014","url":"https://uec.repo.nii.ac.jp/record/9105/files/IPSJ-JNL4602014.pdf"},"version_id":"c7a3b090-5db0-44ae-96f4-5050ed6956c1"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"journal article","resourceuri":"http://purl.org/coar/resource_type/c_6501"}]},"item_title":"分散システム開発におけるモデル検査への視覚的支援手法","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"分散システム開発におけるモデル検査への視覚的支援手法","subitem_title_language":"ja"},{"subitem_title":"Visual Support of Model Checking and Development of Distributed Systems","subitem_title_language":"en"}]},"item_type_id":"10001","owner":"13","path":["6"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2019-04-09"},"publish_date":"2019-04-09","publish_status":"0","recid":"9105","relation_version_is_last":true,"title":["分散システム開発におけるモデル検査への視覚的支援手法"],"weko_creator_id":"13","weko_shared_id":-1},"updated":"2024-03-01T05:23:03.151773+00:00"}