Event-Bを使った時間依存性のあるシステムのモデル化と動作分析のケーススタディ

• Item type: Journal(1)
• 公開日: 2016-08-15
• タイトル: Event-Bを使った時間依存性のあるシステムのモデル化と動作分析のケーススタディ
• タイトル / 言語: en
• タイトル: Modeling and Behavior Analysis Case-study of a Time Dependent System in Event-B
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [特集：組込みシステム工学] Event-B，形式手法，定理証明，時間依存モデル
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 株式会社日立製作所研究開発グループ
• 著者所属: 国立情報学研究所／総合研究大学院大学
• 著者所属(英): en
• 著者所属(英): Research and Development Group, Hitachi, Ltd.
• 著者所属(英): en
• 著者所属(英): National Institute of Informatics / The Graduate University for Advanced Studies, SOKENDAI
• 著者名: 來間, 啓伸; 中島, 震
• 著者名(英): Hironobu, Kuruma; Shin, Nakajima
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 組込みシステムのソフトウェア設計では，環境に起こりうる変化と，それに対するシステムの反応の間の整合性を，網羅的に検証することが重要である．ここで，環境およびシステムの事象の間には，遅延など，時間間隔に関する制約である時間依存性が存在しうるので，それらを考慮した検証を行うことが課題になる．本稿では，自動車ドアロックシステムを題材とした動作分析のケーススタディについて報告し，時間依存性のある事象の間で局所的に時間経過をカウントするモデル化方法を提案する．形式モデリング手法Event-Bを用い，環境の変化とシステムの反応をイベントとして表現する一方，システムが満たすべき要件を不変条件として表した．環境やシステムと独立に進行する共通時間を明示的に導入することなく時間経過をカウントすることで，時間依存性に関わる検証が容易になる．定理証明支援ツールによる不変条件の充足性証明を使って，安全性要件である車速がどのように変化しても一定速度以上であればドアがロックされていることを，形式モデル上で検証することができた．一方，本手法が有効となる検証可能モデルを構成するための方法論の整備が，今後の課題である．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 57, 号 8, p. 1690-1702, 発行日 2016-08-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764