Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code

Dan Zhang, Dragan Bosnacki, Mark van den Brand, Cornelis Huizing, Ruurd Kuiper, Bart Jacobs, Anton Wijs

2016

Abstract

A challenging aspect of model-to-code transformations is to ensure that the semantic behavior of the input model is preserved in the output code. When constructing concurrent systems, this is mainly difficult due to the non-deterministic potential interaction between threads. In this paper, we consider this issue for a framework that implements a transformation chain from models expressed in the state machine based domain specific language SLCO to Java. In particular, we provide a fine-grained generic solution to preserve atomicity of SLCO statements in the Java implementation. We give its generic specification based on separation logic and verify it using the verification tool VeriFast. The solution can be regarded as a reusable module to safely implement atomic operations in concurrent systems.

Paper Citation

in Harvard Style

Zhang D., Bosnacki D., van den Brand M., Huizing C., Kuiper R., Jacobs B. and Wijs A. (2016). Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code . In Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD, ISBN 978-989-758-168-7, pages 578-588. DOI: 10.5220/0005689405780588

in Bibtex Style

@conference{modelsward16,
author={Dan Zhang and Dragan Bosnacki and Mark van den Brand and Cornelis Huizing and Ruurd Kuiper and Bart Jacobs and Anton Wijs},
title={Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code},
booktitle={Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,},
year={2016},
pages={578-588},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005689405780588},
isbn={978-989-758-168-7},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,
TI - Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code
SN - 978-989-758-168-7
AU - Zhang D.
AU - Bosnacki D.
AU - van den Brand M.
AU - Huizing C.
AU - Kuiper R.
AU - Jacobs B.
AU - Wijs A.
PY - 2016
SP - 578
EP - 588
DO - 10.5220/0005689405780588