Verifying atomicity preservation and deadlock freedom of a generic shared variable mechanism used in model-to-code transformations
| Autor: | Zhang, D., Bošnački, D., van den Brand, M.G.J., Huizing, C., Jacobs, B., Kuiper, R., Wijs, A., Hammoudi, S., Pires, L.F., Selic, B., Desfray, P. |
|---|---|
| Přispěvatelé: | Computational Biology |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Atomicity
Separation logic Finite-state machine Java Computer science Concurrency Distributed computing 020207 software engineering 02 engineering and technology Deadlock Deadlock freedom Model transformation Formal verification 020204 information systems 0202 electrical engineering electronic engineering information engineering Code generation computer computer.programming_language |
| Zdroj: | Model-Driven Engineering and Software Development-4th International Conference, MODELSWARD 2016, Revised Selected Papers, 249-273 STARTPAGE=249;ENDPAGE=273;TITLE=Model-Driven Engineering and Software Development-4th International Conference, MODELSWARD 2016, Revised Selected Papers Communications in Computer and Information Science ISBN: 9783319663012 MODELSWARD (Revised Selected Papers) |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|