Towards modular verification of threaded concurrent executable code generated from DSL models

D. Bosnacki, M.G.J. van den Brand, J.M.A.M. Gabriels, B. Jacobs, R. Kuiper, S. Roede, A.J. Wijs, D. Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationFormal Aspects of Component Software
Subtitle of host publication12th International Conference, FACS 2015, Niterói, Brazil, October 14-16, 2015, Revised Selected Papers
EditorsC. Braga, P. Csaba Ölveczky
Place of PublicationDordrecht
PublisherSpringer
Pages141-160
Number of pages20
ISBN (Electronic)978-3-319-28934-2
ISBN (Print)9783319289335
DOIs
Publication statusPublished - 2016
Event12th International Conference on Formal Aspects of Component Software (FACS 2015), October 14-16, 2015, Niterói, Brazil - Niterói, Brazil
Duration: 14 Oct 201516 Oct 2015
http://facs2015.ic.uff.br/

Publication series

NameLecture Notes in Computer Science
Volume9539
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference12th International Conference on Formal Aspects of Component Software (FACS 2015), October 14-16, 2015, Niterói, Brazil
Abbreviated titleFACS 2015
CountryBrazil
CityNiterói
Period14/10/1516/10/15
Internet address

Fingerprint

Dive into the research topics of 'Towards modular verification of threaded concurrent executable code generated from DSL models'. Together they form a unique fingerprint.

Cite this