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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
To avoid ambiguity, in Definition 2, S is called location to distinguish from state variables.
- 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.
VDMJ process is in interactive mode.
- 4.
The VDM-SL model can be downloaded at Overture tool example download page: http://overturetool.org/download/examples/VDMSL/.
- 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
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)
Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press, New York (2009)
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs For Object-Oriented Systems. Springer, Santa Clara (2005)
Fitzgerald, J., Larsen, P.G., Sahara, S.: VDMTools: advances in support for formal modeling in VDM. SIGPLAN Not. 43(2), 3–11 (2008)
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)
Holzmann, G.: SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)
Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64–73 (2014)
Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845–857 (2011)
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)
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall Inc, Upper Saddle River (1990)
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)
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)
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)
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)
Larsen, P.G., Pawlowski, W.: The formal semantics of ISO VDM-SL. Comput. Stand. Interfaces 17(5–6), 585–601 (1995)
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)
Lausdahl, K.: Translating VDM to alloy. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 46–60. Springer, Heidelberg (2013)
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
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)
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
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)
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)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)