|
Title
|
|
|
|
Debugging of model transformations and contracts in SyVOLT
| |
|
Author
|
|
|
|
| |
|
Abstract
|
|
|
|
| The SyVOLT tool verifies DSLTrans transformations by generating a state-space for the transformation’s execution, and then proving structural contracts on that state-space. As with any verification activity, it is non-trivial to ensure that these contracts are error-free and correspond to the user’s intention. SyVOLT detects and localizes errors in the input artefacts for the verification activity to provide the user with assistance in debugging the transformation and/or the contracts. This experience report details the techniques built into the analysis, monitoring, and reporting stages of the tool. These techniques include detection of invalid rules and contracts, a form of reachability analysis during state-space generation, and assist |
| |
|
Language
|
|
|
|
English
| |
|
Publication
|
|
|
|
CEUR-WS
,
2018
| |
|
Volume/pages
|
|
|
|
2245
, p. 532-537
| |
|
Full text (open access)
|
|
|
|
| |
|