| 講演名 | 2015-07-24 SPINを用いたVDM仕様に対するモデル検査適用手法 林 信宏(九大), 大森 洋一(九大), 日下部 茂(九大), 荒木 啓二郎(九大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | VDM (Vienna Development Method)は、形式手法の一つで，ソフトウェア開発の要求に対して様々な抽象レベルの仕様記述が可能である．VDMあるいは形式仕様をソフトウェア開発に適用することは，高品質ソフトウェアに繋ぐ鍵である．しかし，VDMの適用から一番利益を得るためには，VDM仕様の妥当性確認と検証(validation and veification, V&V)が重要である．本稿では，VDMにおける仕様アニメーションの機能を活用してモデル検査の適用手法を提案する．この手法は，VDM仕様アニメーションツールVDMJとモデル検査ツールSPINを持ち合わせしてハイブリットモデルといった検証用モデルを築くことにより，SPINを用いたVDM仕様のモデル検査を実現する． |
| 抄録(英) | The Vienna Development Method (VDM) is a formal method which supports modeling and analysis of software systems at various levels of abstraction. Case studies have shown that applying VDM, or formal specification in general, in software development processes is the key of realizing high quality software development. However, to derive full benefit from the use of VDM in software development, associative activities such as validating and verifying VDM models are crucial. Since the primary way for verifying a VDM model is testing by specification animation, we aim to utilize the animation feature of VDM to apply model checking techniques. In this paper, we propose an approach to support model checking VDM models by constructing a hybrid verification model combining VDMJ, a VDM interpreter, and SPIN model checker. |
| キーワード(和) | VDM / モデル検査 / SPIN |
| キーワード(英) | VDM / Model Checking / SPIN |
| 資料番号 | SS2015-34,KBSE2015-27 |
| 発行日 | 2015-07-15 (SS, KBSE) |
| 研究会情報 | |
| 研究会 | KBSE / SS / IPSJ-SE |
|---|---|
| 開催期間 | 2015/7/22(から3日開催) |
| 開催地（和） | 札幌市教育文化会館 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 委員長氏名（和） | 飯島 正(慶大) / 結縁 祥治(名大) |
| 委員長氏名（英） | Tadashi Iijima(Keio Univ.) / Shoji Yuen(Nagoya Univ.) |
| 副委員長氏名（和） | 金田 重郎(同志社大) / 緒方 和博(北陸先端大) |
| 副委員長氏名（英） | Shigeo Kaneda(Doshisha Univ.) / Kazuhiro Ogata(JAIST) |
| 幹事氏名（和） | 松野 裕(日大) / 中川 博之(阪大) / 小林 隆志(東工大) / 鷲崎 弘宜(早大) |
| 幹事氏名（英） | Yutaka Matsuno(Nihon Univ.) / Hiroyuki Nakagawa(Osaka Univ.) / Takashi Kobayashi(Tokyo Inst. of Tech.) / Hironobu Washizaki(Waseda Univ.) |
| 幹事補佐氏名（和） | 小形 真平(信州大) / 橋浦 弘明(日本工大) / 肥後 芳樹(阪大) |
| 幹事補佐氏名（英） | Shinpei Ogata(Shinshu Univ.) / Hiroaki Hashiura(Nippon Inst. of Tech.) / Yoshiki Higo(Osaka Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Knowledge-Based Software Engineering / Technical Committee on Software Science / Special Interest Group on Software Engineering |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | SPINを用いたVDM仕様に対するモデル検査適用手法 |
| サブタイトル（和） | |
| タイトル（英） | Applying Model Checking on VDM Models using SPIN |
| サブタイトル（和） | |
| キーワード(1)（和/英） | VDM / VDM |
| キーワード(2)（和/英） | モデル検査 / Model Checking |
| キーワード(3)（和/英） | SPIN / SPIN |
| 第 1 著者 氏名（和/英） | 林 信宏 / Hsin-Hung Lin |
| 第 1 著者 所属（和/英） | 九州大学(略称：九大) Kyushu University(略称：Kyushu Univ.) |
| 第 2 著者 氏名（和/英） | 大森 洋一 / Yoichi Omori |
| 第 2 著者 所属（和/英） | 九州大学(略称：九大) Kyushu University(略称：Kyushu Univ.) |
| 第 3 著者 氏名（和/英） | 日下部 茂 / Shigeru Kusakabe |
| 第 3 著者 所属（和/英） | 九州大学(略称：九大) Kyushu University(略称：Kyushu Univ.) |
| 第 4 著者 氏名（和/英） | 荒木 啓二郎 / Keijiro Araki |
| 第 4 著者 所属（和/英） | 九州大学(略称：九大) Kyushu University(略称：Kyushu Univ.) |
| 発表年月日 | 2015-07-24 |
| 資料番号 | SS2015-34,KBSE2015-27 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | SS-153,KBSE-154 |
| ページ範囲 | pp.173-178(SS), pp.173-178(KBSE), |
| ページ数 | 6 |
| 発行日 | 2015-07-15 (SS, KBSE) |