講演抄録/キーワード |
講演名 |
2005-07-25 15:30
SPINによる仕様記述言語の検証 ○堂園隼人・橋本正明・鵜林尚靖・片峯恵一(九工大) |
抄録 |
(和) |
本稿では,ソフトウェア仕様設定の信頼性向上のため,仕様記述言語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. |
キーワード |
(和) |
仕様記述言語 / ルール / 状態遷移図 / SPIN / 仕様検証 / / / |
(英) |
Specification Description Language / Rule / State Transition Diagram / SPIN / Specification Verification / / / |
文献情報 |
信学技報, vol. 105, no. 207, KBSE2005-8, pp. 19-24, 2005年7月. |
資料番号 |
KBSE2005-8 |
発行日 |
2005-07-18 (KBSE) |
ISSN |
Print edition: ISSN 0913-5685 |
PDFダウンロード |
|