{"id":193866,"updated":"2025-01-19T23:47:41.572966+00:00","links":{},"created":"2025-01-19T00:59:00.224438+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00193866","sets":["6164:6165:7019:9662"]},"path":["9662"],"owner":"44499","recid":"193866","title":["NuSMVの反例解析支援ツールの試作"],"pubdate":{"attribute_name":"公開日","attribute_value":"2019-01-17"},"_buckets":{"deposit":"4aeced9f-6d87-4c42-8fe8-802981bc1633"},"_deposit":{"id":"193866","pid":{"type":"depid","value":"193866","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"NuSMVの反例解析支援ツールの試作","author_link":["455113","455109","455105","455108","455106","455107","455111","455110","455114","455112"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"NuSMVの反例解析支援ツールの試作"},{"subitem_title":"A Prototype Tool to Aid Analysis of Counterexamples Produced by NuSMV","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"大規模・不確定システムの自動検証の新潮流","subitem_subject_scheme":"Other"}]},"item_type_id":"18","publish_date":"2019-01-17","item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_18_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"信州大学"},{"subitem_text_value":"信州大学"},{"subitem_text_value":"日本ユニシス株式会社"},{"subitem_text_value":"大阪大学"},{"subitem_text_value":"信州大学"}]},"item_18_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Shinshu University","subitem_text_language":"en"},{"subitem_text_value":"Shinshu University","subitem_text_language":"en"},{"subitem_text_value":"Nihon Unisys, Ltd.","subitem_text_language":"en"},{"subitem_text_value":"Osaka University","subitem_text_language":"en"},{"subitem_text_value":"Shinshu University","subitem_text_language":"en"}]},"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/193866/files/IPSJ-WWS2019007.pdf","label":"IPSJ-WWS2019007.pdf"},"date":[{"dateType":"Available","dateValue":"2021-01-17"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-WWS2019007.pdf","filesize":[{"value":"306.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":"028082db-545f-482b-83ab-60b917c10a94","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2019 by the Information Processing Society of Japan"}]},"item_18_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"大池, 勇太郎"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"小形, 真平"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"青木, 善貴"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"中川, 博之"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"岡野, 浩三"}],"nameIdentifiers":[{}]}]},"item_18_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Yutaro, Oike","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Shinpei, Ogata","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yoshitaka, Aoki","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Hiroyuki, Nakagawa","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Kozo, Okano","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_5794","resourcetype":"conference paper"}]},"item_18_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"モデル検査において，複雑 ・ 大規模なシステムのモデルの反例を手動で解析することは，非常に時間がかかる．NuSMV では反例情報として，状態遷移により変化した変数の値が各状態ごとに出力されるだけであるため，変数の多い大規模なモデルでは開発者による解析が困難になりやすい．本稿では NuSMV から得られた反例解析の効率を向上させるため，反例を自動で変数ごとの遷移を確認できるように, 表形式に整理し保存する．また，反例をグラフとして可視化するためのツールを試作し，セマフォのモデルに対して実行し，誤りのある箇所を絞り込むことに有効な見込みを得られた．","subitem_description_type":"Other"}]},"item_18_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"14","bibliographic_titles":[{"bibliographic_title":"ウィンターワークショップ2019・イン・福島飯坂 論文集"}],"bibliographicPageStart":"13","bibliographicIssueDates":{"bibliographicIssueDate":"2019-01-17","bibliographicIssueDateType":"Issued"},"bibliographicVolumeNumber":"2019"}]},"relation_version_is_last":true,"weko_creator_id":"44499"}}