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 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.
| Original language | English |
|---|---|
| Title of host publication | Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers |
| Editors | S. Hammoudi, L.F. Pires, B. Selic, P. Desfray |
| Publisher | Springer |
| Pages | 249-273 |
| Number of pages | 25 |
| ISBN (Electronic) | 978-3-319-66302-9 |
| ISBN (Print) | 978-3-319-66301-2 |
| DOIs | |
| Publication status | Published - 2017 |
| Event | 4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy: Doctoral Consortium, 20 February 2016 - Rome, Italy Duration: 19 Feb 2016 → 21 Feb 2016 http://www.modelsward.org/DoctoralConsortium.aspx?y=2016 |
Publication series
| Name | Communications in Computer and Information Science |
|---|---|
| Volume | 692 |
| ISSN (Print) | 1865-0929 |
Conference
| Conference | 4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), February 19-21, 2016, Rome, Italy |
|---|---|
| Country | Italy |
| City | Rome |
| Period | 19/02/16 → 21/02/16 |
| Internet address |
Fingerprint
Keywords
- Atomicity
- Code generation
- Concurrency
- Deadlock freedom
- Formal verification
- Model transformation
- Separation logic
Cite this
}
Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations. / Zhang, D.; Bošnački, D.; van den Brand, M.G.J.; Huizing, C.; Jacobs, B.; Kuiper, R.; Wijs, A.
Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers. ed. / S. Hammoudi; L.F. Pires; B. Selic; P. Desfray. Springer, 2017. p. 249-273 (Communications in Computer and Information Science; Vol. 692).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations
AU - Zhang, D.
AU - Bošnački, D.
AU - van den Brand, M.G.J.
AU - Huizing, C.
AU - Jacobs, B.
AU - Kuiper, R.
AU - Wijs, A.
PY - 2017
Y1 - 2017
N2 - 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.
AB - 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.
KW - Atomicity
KW - Code generation
KW - Concurrency
KW - Deadlock freedom
KW - Formal verification
KW - Model transformation
KW - Separation logic
UR - http://www.scopus.com/inward/record.url?scp=85030115904&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-66302-9_13
DO - 10.1007/978-3-319-66302-9_13
M3 - Conference contribution
AN - SCOPUS:85030115904
SN - 978-3-319-66301-2
T3 - Communications in Computer and Information Science
SP - 249
EP - 273
BT - Model-Driven Engineering and Software Development - 4th International Conference, MODELSWARD 2016, Revised Selected Papers
A2 - Hammoudi, S.
A2 - Pires, L.F.
A2 - Selic, B.
A2 - Desfray, P.
PB - Springer
ER -