| 講演名 | 2005-07-25 SPINによる仕様記述言語の検証 堂園 隼人, 橋本 正明, 鵜林 尚靖, 片峯 恵一, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では, ソフトウェア仕様設定の信頼性向上のため, 仕様記述言語e-PSDLを用いて記述された仕様から状態遷移図を抽出し, その状態遷移図をSPINにより検証するための研究について述べる.現在, ソフトウェアは大規模化し, 複雑化しており, 信頼性と生産性の向上が求められている.そのため, 我々は, 仕様の理解性の向上や仕様合成の容易化を目的とした仕様記述言語e-PSDLの言語仕様と, そのプログラムジェネレータの試作を行っている.本稿では, その研究を仕様検証へ発展させ, その検証の一方法を示すとともに, 今後の研究課題を考察する. |
| 抄録(英) | For improving the reliability of software specifications, this article describes the research to extract a state transition diagram from specifications described with a specification description language named e-PSDL and to verify the state transition diagram by SPIN. Recently, software needs the improvement of development methodology because of its increasing scale and complexity. Therefore, we have been studying a specification description language for helping the comprehension and the specification synthesis, and a program generator. This article describes the research on the specification verification and discusses the future study topics. |
| キーワード(和) | 仕様記述言語 / ルール / 状態遷移図 / 仕様検証 |
| キーワード(英) | Specification Description Language / Rule / State Transition Diagram / SPIN / Specification Verification |
| 資料番号 | KBSE2005-8 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 2005/7/18(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | SPINによる仕様記述言語の検証 |
| サブタイトル（和） | |
| タイトル（英） | SPIN-Based Verification of Specifications Described with A Specification Description Language |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 仕様記述言語 / Specification Description Language |
| キーワード(2)（和/英） | ルール / Rule |
| キーワード(3)（和/英） | 状態遷移図 / State Transition Diagram |
| キーワード(4)（和/英） | 仕様検証 / SPIN |
| 第 1 著者 氏名（和/英） | 堂園 隼人 / Hayato Douzono |
| 第 1 著者 所属（和/英） | 九州工業大学 Kyushu Institute of Technology |
| 第 2 著者 氏名（和/英） | 橋本 正明 / Masaaki Hasimoto |
| 第 2 著者 所属（和/英） | 九州工業大学 Kyushu Institute of Technology |
| 第 3 著者 氏名（和/英） | 鵜林 尚靖 / Naoyasu Ubayashi |
| 第 3 著者 所属（和/英） | 九州工業大学 Kyushu Institute of Technology |
| 第 4 著者 氏名（和/英） | 片峯 恵一 / Keiichi Katamine |
| 第 4 著者 所属（和/英） | 九州工業大学 Kyushu Institute of Technology |
| 発表年月日 | 2005-07-25 |
| 資料番号 | KBSE2005-8 |
| 巻番号（vol） | vol.105 |
| 号番号（no） | 207 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |