Towards verifying VDM using SPIN

Hsin Hung Lin, Yoichi Omori, Shigeru Kusakabe, Keijiro Araki

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

1 引用 (Scopus)

抜粋

The Vienna Development Method (VDM) is a formal method that 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 to achieving 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 of verifying a VDM model is specification animation, we aim to utilize the animation feature of VDM to apply model checking techniques. In this paper, we propose an approach to supporting model check VDM models by constructing a hybrid verification model combining VDMJ, a VDM interpreter, and SPIN, one of the most popular model checkers, especially in practical use. Two case studies are reported, and the usability, scalability, and efficiency of our approach are discussed.

元の言語英語
ホスト出版物のタイトルFormal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers
編集者Peter Csaba Ölveczky, Cyrille Artho
出版者Springer Verlag
ページ241-256
ページ数16
ISBN(印刷物)9783319295091
DOI
出版物ステータス出版済み - 1 1 2016
イベント4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015 - Paris, フランス
継続期間: 11 6 201511 7 2015

出版物シリーズ

名前Communications in Computer and Information Science
596
ISSN(印刷物)1865-0929

その他

その他4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015
フランス
Paris
期間11/6/1511/7/15

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Mathematics(all)

フィンガープリント Towards verifying VDM using SPIN' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用

    Lin, H. H., Omori, Y., Kusakabe, S., & Araki, K. (2016). Towards verifying VDM using SPIN. : P. C. Ölveczky, & C. Artho (版), Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers (pp. 241-256). (Communications in Computer and Information Science; 巻数 596). Springer Verlag. https://doi.org/10.1007/978-3-319-29510-7_14