| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2015-07-24 11:40 SPINを用いたVDM仕様に対するモデル検査適用手法 ○林 信宏・大森洋一・日下部 茂・荒木啓二郎（九大）  SS2015-34 KBSE2015-27 |
|
| 抄録 | （和） | 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 / / / / / | |
| 文献情報 | 信学技報, vol. 115, no. 153, SS2015-34, pp. 173-178, 2015年7月. | |
| 資料番号 | SS2015-34 | |
| 発行日 | 2015-07-15 (SS, KBSE) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2015-34 KBSE2015-27 |
|
| 研究会情報 | |
| 研究会 | KBSE SS IPSJ-SE |
| 開催期間 | 2015-07-22 - 2015-07-24 |
| 開催地（和） | 札幌市教育文化会館 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2015-07-KBSE-SS-SE |
| 本文の言語 | 日本語 |
| タイトル（和） | SPINを用いたVDM仕様に対するモデル検査適用手法 |
| サブタイトル（和） | |
| タイトル（英） | Applying Model Checking on VDM Models using SPIN |
| サブタイトル（英） | |
| キーワード(1)（和/英） | VDM / VDM |
| キーワード(2)（和/英） | モデル検査 / Model Checking |
| キーワード(3)（和/英） | SPIN / SPIN |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第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.) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2015-07-24 11:40:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2015-34, KBSE2015-27 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | no.153(SS), no.154(KBSE) |
| ページ範囲 | pp.173-178 |
| ページ数 | 6 |
| 発行日 | 2015-07-15 (SS, KBSE) |
[研究会発表申込システムのトップページに戻る]