{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00186599","sets":["1164:1384:9436:9437"]},"path":["9437"],"owner":"11","recid":"186599","title":["グラフデータベースを用いたモデル検査手法の提案"],"pubdate":{"attribute_name":"公開日","attribute_value":"2018-03-02"},"_buckets":{"deposit":"5de9f2d7-8ba2-419e-9781-0a819076aa0f"},"_deposit":{"id":"186599","pid":{"type":"depid","value":"186599","revision_id":0},"owners":[11],"status":"published","created_by":11},"item_title":"グラフデータベースを用いたモデル検査手法の提案","author_link":["419088","419085","419086","419083","419087","419084"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"グラフデータベースを用いたモデル検査手法の提案"},{"subitem_title":"A Model Checking Approach Using Graph Database","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"モデル検査","subitem_subject_scheme":"Other"}]},"item_type_id":"4","publish_date":"2018-03-02","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"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 University","subitem_text_language":"en"},{"subitem_text_value":"Ibaraki National College of Technology","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/186599/files/IPSJ-SE18198009.pdf","label":"IPSJ-SE18198009.pdf"},"date":[{"dateType":"Available","dateValue":"2020-03-02"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-SE18198009.pdf","filesize":[{"value":"379.9 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":"d23711b6-6fa1-4868-96b0-92178290df81","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2018 by the Information Processing Society of Japan"}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"久野, 和敏"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"上田, 賀一"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"小飼, 敬"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Kazutoshi, Kuno","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yoshikazu, Ueda","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Kei, Kogai","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_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"2188-8825","subitem_source_identifier_type":"ISSN"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"モデル検査において，検査対象の状態数が膨大である場合，現実的な時間で検証できないという問題があり，実用化の課題となっている．先行研究ではこの問題を軽減するため，結合度による振舞いモデルの自動分割と部分状態遷移の生成によって，検査対象の状態数の削減に取り組んだ．しかし，この手法で生成された状態遷移は情報が部分集合化されるため，既存のモデル検査器では検証できない問題が生じた．本研究では，先行研究を用いたモデル検査において，グラフデータベース Neo4j の問い合わせと最小限の状態合成によって，既存のモデル検査器が行う検証と同等な検証を行うための手順を提案する．シミュレーション実験の結果，提案手法による検証が行えることを確認した．","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"In model checking, when the number of states of an object to be inspected is enormous, there is a problem that it can not be verified with realistic time, which is a problem of practical application In previous research, in order to alleviate this problem. we tried to reduce the number of states to be inspected by automatic segmentation of behavior model by degree of coupling and generation of partial state transition. However, since the information is subsetted in the state transition generated by this method, there is a problem that can not be verified by the existing model checker. In this study, we propose a procedure for verification equivalent to verification performed by an existing model checker with by inquiries of the graph database Neo4j and minimal state synthesis of model checking using previous research. As a result of simulation experiments, we confirmed that we can verify by the proposed method.","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":"2018-03-02","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"9","bibliographicVolumeNumber":"2018-SE-198"}]},"relation_version_is_last":true,"weko_creator_id":"11"},"id":186599,"updated":"2025-01-20T02:31:14.121393+00:00","links":{},"created":"2025-01-19T00:53:32.501075+00:00"}