Automated Translation Of Vdm To Jml-Annotated Java

Keywords

Code-generation; Design-by-Contract; Formal methods; Java; JML; VDM

Abstract

When a system specified using the Vienna Development Method (VDM) is realised using code-generation, no guarantees are currently made about the correctness of the generated code. In this paper, we improve code-generation of VDM models by taking contract-based elements such as invariants and pre- and postconditions into account during the code-generation process. The contract-based elements of the Vienna Development Method Specification Language (VDM-SL) are translated into corresponding constructs in the Java Modelling Language (JML) and used to validate the generated code against the properties of the VDM model. VDM-SL and JML are both Design-by-Contract (DbC) languages, with the difference that VDM-SL supports abstract modelling and system specification, while JML is used for detailed specification of Java classes and interfaces. We describe the semantic differences between the contract-based elements of VDM-SL and JML and formulate the translation as a set of rules. We further demonstrate how dynamic JML assertion checks can be used to ensure the consistency of VDM’s subtypes when a model is code-generated. The translator is fully automated and produces JML-annotated Java programs that can be checked for correctness using JML tools.

Publication Date

4-1-2018

Publication Title

International Journal on Software Tools for Technology Transfer

Volume

20

Issue

2

Number of Pages

211-235

Document Type

Article

Personal Identifier

scopus

DOI Link

https://doi.org/10.1007/s10009-017-0448-3

Socpus ID

85012146687 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/85012146687

This document is currently not available here.

Share

COinS