| Presentation | 2015-07-24 Applying Model Checking on VDM Models using SPIN Hsin-Hung Lin, Yoichi Omori, Shigeru Kusakabe, Keijiro Araki, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | VDM / Model Checking / SPIN |
| Paper # | SS2015-34,KBSE2015-27 |
| Date of Issue | 2015-07-15 (SS, KBSE) |
| Conference Information | |
| Committee | KBSE / SS / IPSJ-SE |
|---|---|
| Conference Date | 2015/7/22(3days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Tadashi Iijima(Keio Univ.) / Shoji Yuen(Nagoya Univ.) |
| Vice Chair | Shigeo Kaneda(Doshisha Univ.) / Kazuhiro Ogata(JAIST) |
| Secretary | Shigeo Kaneda(Nihon Univ.) / Kazuhiro Ogata(Osaka Univ.) / (Tokyo Inst. of Tech.) |
| Assistant | Shinpei Ogata(Shinshu Univ.) / Hiroaki Hashiura(Nippon Inst. of Tech.) / Yoshiki Higo(Osaka Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Knowledge-Based Software Engineering / Technical Committee on Software Science / Special Interest Group on Software Engineering |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Applying Model Checking on VDM Models using SPIN |
| Sub Title (in English) | |
| Keyword(1) | VDM |
| Keyword(2) | Model Checking |
| Keyword(3) | SPIN |
| 1st Author's Name | Hsin-Hung Lin |
| 1st Author's Affiliation | Kyushu University(Kyushu Univ.) |
| 2nd Author's Name | Yoichi Omori |
| 2nd Author's Affiliation | Kyushu University(Kyushu Univ.) |
| 3rd Author's Name | Shigeru Kusakabe |
| 3rd Author's Affiliation | Kyushu University(Kyushu Univ.) |
| 4th Author's Name | Keijiro Araki |
| 4th Author's Affiliation | Kyushu University(Kyushu Univ.) |
| Date | 2015-07-24 |
| Paper # | SS2015-34,KBSE2015-27 |
| Volume (vol) | vol.115 |
| Number (no) | SS-153,KBSE-154 |
| Page | pp.pp.173-178(SS), pp.173-178(KBSE), |
| #Pages | 6 |
| Date of Issue | 2015-07-15 (SS, KBSE) |