{"id":174243,"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00174243","sets":["581:8417:8426"]},"path":["8426"],"owner":"11","recid":"174243","title":["Event-Bを使った時間依存性のあるシステムのモデル化と動作分析のケーススタディ"],"pubdate":{"attribute_name":"公開日","attribute_value":"2016-08-15"},"_buckets":{"deposit":"173e4a01-184f-44c3-9907-fe9dc724472f"},"_deposit":{"id":"174243","pid":{"type":"depid","value":"174243","revision_id":0},"owners":[11],"status":"published","created_by":11},"item_title":"Event-Bを使った時間依存性のあるシステムのモデル化と動作分析のケーススタディ","author_link":["356754","356756","356755","356757"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Event-Bを使った時間依存性のあるシステムのモデル化と動作分析のケーススタディ"},{"subitem_title":"Modeling and Behavior Analysis Case-study of a Time Dependent System in Event-B","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"[特集：組込みシステム工学] Event-B，形式手法，定理証明，時間依存モデル","subitem_subject_scheme":"Other"}]},"item_type_id":"2","publish_date":"2016-08-15","item_2_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"株式会社日立製作所研究開発グループ"},{"subitem_text_value":"国立情報学研究所／総合研究大学院大学"}]},"item_2_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Research and Development Group, Hitachi, Ltd.","subitem_text_language":"en"},{"subitem_text_value":"National Institute of Informatics / The Graduate University for Advanced Studies, SOKENDAI","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"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/174243/files/IPSJ-JNL5708004.pdf","label":"IPSJ-JNL5708004.pdf"},"date":[{"dateType":"Available","dateValue":"2018-08-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-JNL5708004.pdf","filesize":[{"value":"930.7 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":"8"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"ac266b8e-b2d7-4c39-830a-de523cee2d02","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2016 by the Information Processing Society of Japan"}]},"item_2_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"來間, 啓伸"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"中島, 震"}],"nameIdentifiers":[{}]}]},"item_2_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Hironobu, Kuruma","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Shin, Nakajima","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_2_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN00116647","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_2_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7764","subitem_source_identifier_type":"ISSN"}]},"item_2_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"組込みシステムのソフトウェア設計では，環境に起こりうる変化と，それに対するシステムの反応の間の整合性を，網羅的に検証することが重要である．ここで，環境およびシステムの事象の間には，遅延など，時間間隔に関する制約である時間依存性が存在しうるので，それらを考慮した検証を行うことが課題になる．本稿では，自動車ドアロックシステムを題材とした動作分析のケーススタディについて報告し，時間依存性のある事象の間で局所的に時間経過をカウントするモデル化方法を提案する．形式モデリング手法Event-Bを用い，環境の変化とシステムの反応をイベントとして表現する一方，システムが満たすべき要件を不変条件として表した．環境やシステムと独立に進行する共通時間を明示的に導入することなく時間経過をカウントすることで，時間依存性に関わる検証が容易になる．定理証明支援ツールによる不変条件の充足性証明を使って，安全性要件である車速がどのように変化しても一定速度以上であればドアがロックされていることを，形式モデル上で検証することができた．一方，本手法が有効となる検証可能モデルを構成するための方法論の整備が，今後の課題である．","subitem_description_type":"Other"}]},"item_2_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"Proving the consistency between the system's responses and the changes that may occur in its environment is an important task in software design verification of embedded systems. Since the phoenomena in a system and its environment are generally related through the progress of time, modeling of time is a problem to be solved in constructing models of systems and environments. In this paper, we pick up a car door lock system and report a case study of formal modeling and behavior analysis. We propose a modeling method for time dependent systems in which the progress of time is counted locally by concerning events. The changes in the environment and the responses of the system are modeled as events and the properties which the system should maintain are modeled as invariants in Event-B. Since the time dependency between events are represented without introducing actual time, the verification processes of timing properties become simpler. We show a safety property, the doors are always locked when the velocity of the car exceeds a fixed value, is proved independent of the acceleration and deceleration patterns. Our future work is to develop a methodology for constructing verifiable time dependent models.","subitem_description_type":"Other"}]},"item_2_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"1702","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌"}],"bibliographicPageStart":"1690","bibliographicIssueDates":{"bibliographicIssueDate":"2016-08-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"8","bibliographicVolumeNumber":"57"}]},"relation_version_is_last":true,"weko_creator_id":"11"},"updated":"2025-01-20T06:58:08.418075+00:00","created":"2025-01-19T00:44:27.881428+00:00","links":{}}