Skip to main content
SpringerLink
Log in

Towards Verifying VDM Using SPIN

  • Conference paper
  • First Online:
Formal Techniques for Safety-Critical Systems (FTSCS 2015)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 596))

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.

This work was partly supported by KAKENHI, Grant-in-Aid for Scientific Research(S) 24220001.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    To avoid ambiguity, in Definition 2, S is called location to distinguish from state variables.

  2. 2.

    We skipped the detail of sel_mynat_param which is used to enumerate the input of operations: a set of myNat containing one or two digits (0–9).

  3. 3.

    VDMJ process is in interactive mode.

  4. 4.

    The VDM-SL model can be downloaded at Overture tool example download page: http://overturetool.org/download/examples/VDMSL/.

  5. 5.

    There are two clocks of type nat in the state variables defined in module SAFER and AAH we found that only two cases were worth considering in the verification.

References

  1. VDMJ. http://sourceforge.net/projects/vdmj/

  2. Agerholm, S., Larsen, P.G.: Modeling and validating SAFER in VDM-SL. In: Proceedings of the Fourth NASA Langley Formal Methods Workshop, NASA Conference, Publication 3356 (1997)

    Google Scholar 

  3. Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978)

    MATH  Google Scholar 

  4. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  5. Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press, New York (2009)

    Book  Google Scholar 

  6. Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs For Object-Oriented Systems. Springer, Santa Clara (2005)

    MATH  Google Scholar 

  7. Fitzgerald, J., Larsen, P.G., Sahara, S.: VDMTools: advances in support for formal modeling in VDM. SIGPLAN Not. 43(2), 3–11 (2008)

    Article  Google Scholar 

  8. Fröhlich, B., Larsen, P.: Combining VDM-SL specifications with C++ code. In: Gaudel, M.C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 179–194. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  9. Holzmann, G.: SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)

    Google Scholar 

  10. Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64–73 (2014)

    Article  Google Scholar 

  11. Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845–857 (2011)

    Article  Google Scholar 

  12. Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 76–91. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall Inc, Upper Saddle River (1990)

    MATH  Google Scholar 

  14. Kurita, T., Chiba, M., Nakatsugawa, Y.: Application of a formal specification language in the development of the “Mobile FeliCa” IC chip firmware for embedding in mobile phone. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 425–429. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Kurita, T., Nakatsugawa, Y.: The application of VDM to the industrial development of firmware for a smart card IC chip. Int. J. Softw. Inf. 3(2–3), 343–355 (2009)

    Google Scholar 

  16. Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative integrating tools for VDM. SIGSOFT Softw. Eng. Notes 35(1), 1–6 (2010)

    Article  Google Scholar 

  17. Larsen, P.G., Fitzgerald, J.: Recent industrial applications of VDM in Japan. In: Proceedings of the 2007th Internatioanal Conference on Formal Methods in Industry, FACS-FMI 2007, p. 8. British Computer Society, Swinton (2007)

    Google Scholar 

  18. Larsen, P.G., Pawlowski, W.: The formal semantics of ISO VDM-SL. Comput. Stand. Interfaces 17(5–6), 585–601 (1995)

    Article  Google Scholar 

  19. Larsen, P., Lassen, P.: An executable subset of meta-IV with loose specification. In: Prehn, S., Toetenel, W. (eds.) VDM 1991. LNCS, vol. 551, pp. 604–618. Springer, Berlin Heidelberg (1991)

    Google Scholar 

  20. Lausdahl, K.: Translating VDM to alloy. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 46–60. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  21. Lausdahl, K., Ishikawa, H., Larsen, P.G.: Interpreting implicit VDM specifications using ProB. In: Battle, N., Fitzgerald, J. (eds.) Proceedings of the 12th Overture Workshop, Newcastle University, 21 June, 2014. School of Computing Science, Newcastle University, UK, Technical report CS-TR-1446, January 2015

    Google Scholar 

  22. Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Berlin Heidelberg (2003)

    Google Scholar 

  23. Nakatsugawa, Y., Kurita, T., Araki, K.: A framework for formal specification considering review and specification-based testing. In: TENCON 2010–2010 IEEE Region 10 Conference, pp. 2444–2448, November 2010

    Google Scholar 

  24. Lausdahl, K., Larsen, P.G., Nielsen, C.B.: Combining VDM with executable code. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 266–279. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  25. Triska, M.: The finite domain constraint solver of SWI-Prolog. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 307–316. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  26. Larsen, P.G., Hooman, J., Verhoef, M.: Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 147–162. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Science and Electrical Engineering, Kyushu University, Fukuoka, Japan

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

Authors
  1. Hsin-Hung Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yoichi Omori
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shigeru Kusakabe
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Keijiro Araki
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hsin-Hung Lin .

Editor information

Editors and Affiliations

  1. AIST Ikeda, Ikeda,Osaka, Japan

    Cyrille Artho

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Lin, HH., Omori, Y., Kusakabe, S., Araki, K. (2016). Towards Verifying VDM Using SPIN. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2015. Communications in Computer and Information Science, vol 596. Springer, Cham. https://doi.org/10.1007/978-3-319-29510-7_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29510-7_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29509-1

  • Online ISBN: 978-3-319-29510-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation