Combining VDM with Executable Code

Abstract

Formal methods have been used and successfully applied to a wide range of industrial applications for many years. However formal methods can be difficult to comprehend for outsiders and the link of formal models and external subsystems which are not modelled can be unclear. In this paper we present an approach which allows formal models to be more easily shared with external stakeholders and enables integration with external code. We demonstrate how an existing interpreter for an executable subset of VDM is extended enabling the combination of formal models with executable code. This eases the way in which a formal model can communicate with an external implementation or be used in graphical prototyping. A small case study is used to demonstrate how the approach can be utilized. In this paper the technique is used to combine VDM and Java, but the principles presented can be seen as a general approach for expanding the capabilities of formal modelling tools with interpretation capabilities.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{NielsenLL12,
  author       = {Claus Ballegaard Nielsen and
                  Kenneth Lausdahl and
                  Peter Gorm Larsen},
  editor       = {John Derrick and
                  John S. Fitzgerald and
                  Stefania Gnesi and
                  Sarfraz Khurshid and
                  Michael Leuschel and
                  Steve Reeves and
                  Elvinia Riccobene},
  title        = {Combining {VDM} with Executable Code},
  booktitle    = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
                  Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7316},
  pages        = {266--279},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-30885-7\_19},
  doi          = {10.1007/978-3-642-30885-7\_19},
  timestamp    = {Sun, 02 Jun 2019 21:23:59 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/NielsenLL12.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}