ユーザタスクの形式的記述に基づくインタラクティブシステム設計法

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12680350
• Research Institution: NARA INSTITUTE OF SCIENCE AND TECHNOLOGY
• Principal Investigator: 関 浩之 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80196948)
• Co-Investigator(Kenkyū-buntansha): 高田 喜朗 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (60294279)
• Keywords: ユーザインタフェース / インタラクティブシステム / 形式的検証 / プロトタイプ自動生成 / タスク図 / 代数的仕様 / 抽象的順序機械

Research Abstract

1.昨年度に引き続き,タスク図を用いたインタラクティブシステム設計法についての研究を行った.昨年度は主に,ユーザタスクに基づく設計法,タスク図を用いた仕様記述法,および,詳細化されたタスク図からのプロトタイプ自動生成法を提案した.本年度は,タスク図の形式的意味定義とその形式的検証法への応用について詳細に検討した.
(a)プロセス代数に基づく代表的な仕様記述言語であるLOTOSに着目し,タスク図からLOTOS仕様への変換規則を与えることにより,タスク図の形式的意味を定義した.
(b)与えられたタスク図を上記変換規則によりLOTOS仕様に変換し,次に,モデル検査法に基づく検証ツールであるCADPを用いてLOTOS仕様を検証するという,タスク図の形式的検証手順を示した.通信販売による書籍購入タスクに提案検証法を適用することにより,その有効性を示した.
2.ユーザインタフェース(UI)部品の厳密な仕様記述を可能とする設計法として,代数的仕様記述法を用いた設計法を提案した.具体的に,代数的仕様記述の部分クラスである抽象的順序機械型仕様(ASM仕様)を用いたUIの形式的仕様記述法とそこからのプロトタイプ生成法を提案した.まず,個々のUIモジュールがメッセージ送受信によって非同期に動作するような,簡潔な多プロセスモデルである抽象的ウィンドウシステム(AWS)モデルを導入した.次に,AWSに基づきUIのASM仕様を記述する方法を示した.また,Javaを実装アーキテクチャとした,UIのASM仕様を実装するための枠組を提案した.この枠組に従ってASM仕様をJavaプログラムに変換するコンパイラを作成し,仕様記述例に対するコンパイラの仕様経験から,本手法の有効性を確認した.

Research Products

• [Publications] 池田瑞穂, 高田喜朗, 関浩之: "インタラクティブシステム設計法におけるタスクモデルの形式的記述と検証"電子通信学会技術研究報告. SS2001-12. 1-8 (2001)
• [Publications] Mizuho Ikeda, Yoshiaki Takada, Hiroyuki Seki: "Formal Specification and Implementation Using a Task Flow Diagram In Interactive System Design"5^<th> World Multiconference on Systemics, Cybernetics and Informatics. I. 422-428 (2001)
• [Publications] 池田瑞穂, 高田喜朗, 関浩之: "ユーザインタフェースの代数的仕様記述と仕様からのプログラム生成"情報処理学会研究報告. 2001-SE-135. 9-16 (2001)
• [Publications] 池田瑞穂, 高田喜朗, 関浩之: "インタラクティブシステム設計法におけるタスク図の形式的意味定義と形式的検証への応用"コンピュータソフトウェア. Vol.19,No.2(印刷中). (2002)