| 講演名 | 2001/7/23 インタラクティブシステム設計法におけるタスクモデルの形式的記述と検証 池田 瑞穂, 高田 喜朗, 関 浩之, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 著者らは, インタラクティブシステムの設計手法として, ユーザのタスクモデルに基づく形式的仕様を用いた設計法を提案している.本稿では, タスクモデルの記述法であるタスク図を, データ属性を導入することによって拡張し, LOTOS仕様への変換規則を与えることにより, タスク図の形式的意味を定義した.LOTOS仕様に対するモデル検査法を用いることにより, タスク図で記述されたタスクモデルの形式的検証手順を示した.そして, 例題に対して形式的検証を行い, その有効性を確認した。 |
| 抄録(英) | The authors proposed a design method of interactive systems in which a formal specification of a user's task is used. In this paper, we extend the specification language-task flow diagram-by introducing data attributes of tasks and define the semantics of a task flow diagram by a translation into a LOTOS specification. Also we present a verification procedure of a task model using a model checking tool for LOTOS specifications. Verification results on a sample task model are presented. |
| キーワード(和) | モデル検査法 / LOTOS / タスクモデル / インタラクティブシステム / 形式的検証 |
| キーワード(英) | model checking / LOTOS / task model / interactive system / formal verification |
| 資料番号 | SS2001-12 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2001/7/23(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | インタラクティブシステム設計法におけるタスクモデルの形式的記述と検証 |
| サブタイトル（和） | |
| タイトル（英） | Verification of a Task Model based on the Formal Definition of a Task Flow Diagram |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査法 / model checking |
| キーワード(2)（和/英） | LOTOS / LOTOS |
| キーワード(3)（和/英） | タスクモデル / task model |
| キーワード(4)（和/英） | インタラクティブシステム / interactive system |
| キーワード(5)（和/英） | 形式的検証 / formal verification |
| 第 1 著者 氏名（和/英） | 池田 瑞穂 / Mizuho Ikeda |
| 第 1 著者 所属（和/英） | 奈良先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Nara Institute of Science and Technology |
| 第 2 著者 氏名（和/英） | 高田 喜朗 / Yoshiaki Takata |
| 第 2 著者 所属（和/英） | 奈良先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Nara Institute of Science and Technology |
| 第 3 著者 氏名（和/英） | 関 浩之 / Hiroyuki Seki |
| 第 3 著者 所属（和/英） | 奈良先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Nara Institute of Science and Technology |
| 発表年月日 | 2001/7/23 |
| 資料番号 | SS2001-12 |
| 巻番号（vol） | vol.101 |
| 号番号（no） | 240 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |