Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

2 Citaten (Scopus)
2 Downloads (Pure)

Samenvatting

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 mechanism 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. Moreover, we also prove with VeriFast that our mechanism does not introduce deadlocks. The specification formally ensures that the locks are not reentrant which simplifies the formal treatment of the Java locks.

Originele taal-2Engels
TitelModel-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers
RedacteurenS. Hammoudi, L.F. Pires, B. Selic, P. Desfray
UitgeverijSpringer
Pagina's249-273
Aantal pagina's25
ISBN van elektronische versie978-3-319-66302-9
ISBN van geprinte versie978-3-319-66301-2
DOI's
StatusGepubliceerd - 2017
Evenement4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy: Doctoral Consortium, 20 February 2016 - Rome, Italië
Duur: 19 feb 201621 feb 2016
http://www.modelsward.org/DoctoralConsortium.aspx?y=2016

Publicatie series

NaamCommunications in Computer and Information Science
Volume692
ISSN van geprinte versie1865-0929

Congres

Congres4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy
LandItalië
StadRome
Periode19/02/1621/02/16
Internet adres

Vingerafdruk Duik in de onderzoeksthema's van 'Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Zhang, D., Bošnački, D., van den Brand, M. G. J., Huizing, C., Jacobs, B., Kuiper, R., & Wijs, A. (2017). Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations. In S. Hammoudi, L. F. Pires, B. Selic, & P. Desfray (editors), Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers (blz. 249-273). (Communications in Computer and Information Science; Vol. 692). Springer. https://doi.org/10.1007/978-3-319-66302-9_13