Verification of atomicity preservation in model-to-code transformations using generic Java code

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 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.

Originele taal-2Engels
TitelMODELSWARD 2016 - Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development
UitgeverijSCITEPRESS-Science and Technology Publications, Lda.
Pagina's578-588
Aantal pagina's11
ISBN van geprinte versie9789897581687
DOI's
StatusGepubliceerd - 2016
Evenement4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016) - Rome, Italië
Duur: 19 feb 201621 feb 2016
http://www.modelsward.org/?y=2016

Congres

Congres4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016)
Verkorte titelMODELSWARD 2016
LandItalië
StadRome
Periode19/02/1621/02/16
Internet adres

Vingerafdruk Duik in de onderzoeksthema's van 'Verification of atomicity preservation in model-to-code transformations using generic Java code'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Zhang, D., Bosnacki, D., Van Den Brand, M., Huizing, C., Kuiper, R., Jacobs, B., & Wijs, A. (2016). Verification of atomicity preservation in model-to-code transformations using generic Java code. In MODELSWARD 2016 - Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development (blz. 578-588). SCITEPRESS-Science and Technology Publications, Lda.. https://doi.org/10.5220/0005689405780588