Abstract
When applying model-driven engineering to safety-critical systems, the correctness of model transformations is crucial. In this paper, we investigate a novel approach to verifying the conformance to source language semantics of model-to-code transformations that uses annotations in the generated code. These annotations are inserted by the transformation and are used to guide a model checker to verify that the generated code satisfies the semantics of the source language - UML state machines in this paper. Verifying the generated output in this way is more efficient than formally verifying the transformation's definition. The verification is performed using Java Pathfinder (JPF) [1], a model checker for Java source code. The approach has been applied to verify three UML state machine to Java code generators: one developed by us and two commercial generators (Rhapsody and Visual Paradigm). We were able to detect non-conformance in both commercial tools, which failed some semantic properties extracted from the UML specification.
Original language | English |
---|---|
Title of host publication | Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings |
Pages | 166-180 |
Number of pages | 15 |
Volume | 6394 LNCS |
Edition | PART 1 |
DOIs | |
Publication status | Published - 2010 |
Externally published | Yes |
Event | ACM/IEEE International Conference on Model Driven Engineering Languages and Systems 2010 - Oslo, Norway Duration: 3 Oct 2010 → 8 Oct 2010 Conference number: 13th https://dl.acm.org/doi/proceedings/10.5555/1926458 (Proceedings) |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Number | PART 1 |
Volume | 6394 LNCS |
ISSN (Print) | 03029743 |
ISSN (Electronic) | 16113349 |
Conference
Conference | ACM/IEEE International Conference on Model Driven Engineering Languages and Systems 2010 |
---|---|
Abbreviated title | MoDELS 2010 |
Country/Territory | Norway |
City | Oslo |
Period | 3/10/10 → 8/10/10 |
Internet address |
|