物理的相互作用に着目したスマート空間の形式仕様記述と検証

IPSJ

Bibliographic Information

Other Title
  • Formal Specification and Verification of Smart Spaces: Focusing on Physical Interactions

Search this article

Abstract

開発プロセスの早期においては，不整合や抜け等の誤りが後の過程に引き継がれ手戻りを引き起こすことを避けるため，系統的なモデル化・分析を行うことが信頼性，効率性の観点から重要である．しかし従来のソフトウェア開発に比べて，スマート空間の開発については早期のモデル化・分析手法が確立されていない．本論文においては，スマート空間仕様の早期モデル化と，モデル検査によるその検証のためのフレームワークを提案する．提案フレームワークにおいては，ユーザとデバイス間の視覚，聴覚等の物理的な相互作用の抽象モデル化に基づいたスマート空間仕様記述言語を提供する．また，特に計算機により制御できないユーザの存在を考慮した検証項目について，既存ツールSPINを用いたモデル検査を行う仕組みを提供する．また，抽象的な仕様の分析と修正・追加をインタラクティブに，また段階的に繰り返す過程における提案フレームワークの有用性について，ケーススタディを通して確認した．

Systematic modeling and analysis methods in early phases of the development process are essential for reliable and efficient system development, in order to prevent deficiencies from being inherited to later phases and causing costly rollback. However, such methods have not been intensively explored for smart spaces, compared with traditional software engineering. This paper proposes a framework for early modeling of smart spaces specifications as well as verification by model checking. The framework includes a modeling language for smart space specifications based on abstract modeling of physical interactions between users and devices, e.g., visual or audio interactions. The framework also includes a mechanism for model checking of the specifications, against specific properties that reflect uncontrollability of users, through translation to inputs for an existing tool, SPIN. Case studies are conducted to discuss usefulness of the proposed framework in interactive analysis and modification of abstract specifications.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top