Details

Autor(en) / Beteiligte

• Braga, Christiano
• Ölveczky, Peter Csaba

Titel

Towards Modular Verification of Threaded Concurrent Executable Code Generated from DSL Models

Ist Teil von

• Formal Aspects of Component Software, 2016, Vol.9539, p.141-160

Ort / Verlag

Switzerland: Springer International Publishing AG

Erscheinungsjahr

2016

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• An important problem in Model Driven Engineering is maintaining the correctness of a specification under model transformations. We consider this issue for a framework that implements the transformation chain from the modeling language SLCO to Java. In particular, we verify the generic part of the last transformation step to Java code, involving change in granularity, focusing on the implementation of SLCO communication channels. To this end we use a parameterized modular approach; we apply a novel proof schema that supports fine grained concurrency and procedure-modularity, and use the separation logic based tool VeriFast. Our results show that such tool-assisted formal verification can be a viable addition to traditional techniques, supporting object orientation, concurrency via threads, and parameterized verification.