Name
Title | ||
|---|---|---|
Towards Modular Verification of Threaded Concurrent Executable Code Generated from DSL Models. |
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-28934-2_8 | FACS |
Field | DocType | Volume |
Separation logic,Programming language,Model-driven architecture,Concurrency,Computer science,Correctness,Modeling language,Java,Formal verification,Distributed computing,Executable | Conference | 9539 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.39 |
References | Authors | |
13 | 8 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dragan Bosnacki | 1 | 276 | 26.95 |
| Mark Van Den Brand | 2 | 1298 | 110.20 |
| Joost Gabriels | 3 | 2 | 0.39 |
| Bart Jacobs 0002 | 4 | 22 | 6.28 |
| Ruurd Kuiper | 5 | 566 | 105.58 |
| Sybren Roede | 6 | 2 | 0.39 |
| Anton Wijs | 7 | 203 | 22.84 |
| Dan Zhang | 8 | 4 | 1.79 |