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