Towards verifying VDM using SPIN

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (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.

Original languageEnglish
Title of host publicationFormal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers
EditorsPeter Csaba Ölveczky, Cyrille Artho
PublisherSpringer Verlag
Number of pages16
ISBN (Print)9783319295091
Publication statusPublished - 2016
Event4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015 - Paris, France
Duration: Nov 6 2015Nov 7 2015

Publication series

NameCommunications in Computer and Information Science
ISSN (Print)1865-0929


Other4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Mathematics(all)


Dive into the research topics of 'Towards verifying VDM using SPIN'. Together they form a unique fingerprint.

Cite this