{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00226853","sets":["1164:1384:11164:11267"]},"path":["11267"],"owner":"44499","recid":"226853","title":["二種類のモデル検査器を用いたシステムの振る舞いの検証の試み"],"pubdate":{"attribute_name":"公開日","attribute_value":"2023-07-13"},"_buckets":{"deposit":"e1c2076b-6b04-4543-8e21-4e1cc0ddd7ea"},"_deposit":{"id":"226853","pid":{"type":"depid","value":"226853","revision_id":0},"owners":[44499],"status":"published","created_by":44499},"item_title":"二種類のモデル検査器を用いたシステムの振る舞いの検証の試み","author_link":["603235","603238","603233","603232","603239","603234","603237","603236"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"二種類のモデル検査器を用いたシステムの振る舞いの検証の試み"},{"subitem_title":"Verification of System Behavior using two types of model checking","subitem_title_language":"en"}]},"item_type_id":"4","publish_date":"2023-07-13","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"BIPROGY株式会社"},{"subitem_text_value":"信州大学"},{"subitem_text_value":"大阪大学"},{"subitem_text_value":"信州大学"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":" BIPROGY Inc.","subitem_text_language":"en"},{"subitem_text_value":"Shinshu University","subitem_text_language":"en"},{"subitem_text_value":"Osaka University","subitem_text_language":"en"},{"subitem_text_value":"Shinshu University","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/226853/files/IPSJ-SE23214027.pdf","label":"IPSJ-SE23214027.pdf"},"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-SE23214027.pdf","filesize":[{"value":"1.3 MB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"12"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_login","version_id":"93ad56e4-058e-49fb-b20a-80a1dd8f0f52","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2023 by the Institute of Electronics, Information and Communication Engineers This SIG report is only available to those in membership of the SIG."}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"青木, 善貴"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"小形, 真平"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"中川, 博之"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"小林, 一樹"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Yoshitaka, Aoki","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Shinpei, Ogata","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Hiroyuki, Nakagawa","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Kazuki, Kobayashi","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":"モデル検査は，複雑な相互作用をもつシステムの性質を検証に有効である．NuSMV や SPIN などのモデル検査器はそういった複雑なモデルの振る舞いの検証には適しているが，時間的な考慮が必要な検証をすることはできない．本稿では，モデル検査器の NuSMV と時間を扱えるモデル検査器 PRISM を併用することにより，複雑な相互作用をもつモデルに，時間的な考慮を入れた検証ができる手法を提案する．","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"In recent years, with the development of interfaces, the number of systems that interact closely with humans has increased. With the development of networks, multimodal user interfaces have been developed. Conflicts in the operation of multiple interfaces can lead system behavior that is contrary to human expectation, and the behavior may cause serious accidents. Model checking is effective in verifying properties of systems with complex interactions. Model checkers such as NuSMV and SPIN are suitable for verifying the behavior of such complex models, but they cannot perform time-sensitive verifications. In this paper, we propose a verification method that considers time for models with complex interactions by using both NuSMV, a model checker, and PRISM, a model checker that can handle time.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"6","bibliographic_titles":[{"bibliographic_title":"研究報告ソフトウェア工学（SE）"}],"bibliographicPageStart":"1","bibliographicIssueDates":{"bibliographicIssueDate":"2023-07-13","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"27","bibliographicVolumeNumber":"2023-SE-214"}]},"relation_version_is_last":true,"weko_creator_id":"44499"},"id":226853,"updated":"2025-01-19T12:21:26.551682+00:00","links":{},"created":"2025-01-19T01:26:10.653017+00:00"}