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)

Abstract

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
Pages241-256
Number of pages16
ISBN (Print)9783319295091
DOIs
Publication statusPublished - Jan 1 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
Volume596
ISSN (Print)1865-0929

Other

Other4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015
CountryFrance
CityParis
Period11/6/1511/7/15

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Mathematics(all)

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

  • Cite this

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