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

• Item type: Journal(1)
• 公開日: 2011-01-15
• タイトル: 物理的相互作用に着目したスマート空間の形式仕様記述と検証
• タイトル / 言語: en
• タイトル: Formal Specification and Verification of Smart Spaces: Focusing on Physical Interactions
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 特集：魅力ある情報通信社会のためのモバイル通信と高度交通システム
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 国立情報学研究所GRACEセンター
• 著者所属: 日立製作所
• 著者所属: 国立情報学研究所GRACEセンター／東京大学
• 著者所属(英): en
• 著者所属(英): GRACE Center, National Institute of Informatics
• 著者所属(英): en
• 著者所属(英): Hitachi, Ltd.
• 著者所属(英): en
• 著者所属(英): GRACE Center, National Institute of Informatics / The University of Tokyo
• 著者名: 石川, 冬樹; 山本, 佳代子; 本位田真一
• 著者名(英): Fuyuki, Ishikawa; Kayoko, Yamamoto; Shinichi, Honiden
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 開発プロセスの早期においては，不整合や抜け等の誤りが後の過程に引き継がれ手戻りを引き起こすことを避けるため，系統的なモデル化・分析を行うことが信頼性，効率性の観点から重要である．しかし従来のソフトウェア開発に比べて，スマート空間の開発については早期のモデル化・分析手法が確立されていない．本論文においては，スマート空間仕様の早期モデル化と，モデル検査によるその検証のためのフレームワークを提案する．提案フレームワークにおいては，ユーザとデバイス間の視覚，聴覚等の物理的な相互作用の抽象モデル化に基づいたスマート空間仕様記述言語を提供する．また，特に計算機により制御できないユーザの存在を考慮した検証項目について，既存ツールSPINを用いたモデル検査を行う仕組みを提供する．また，抽象的な仕様の分析と修正・追加をインタラクティブに，また段階的に繰り返す過程における提案フレームワークの有用性について，ケーススタディを通して確認した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 52, 号 1, p. 220-232, 発行日 2011-01-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764