Verifying semantic conformance of state machine-to-Java code generators

Lukman Ab. Rahim, Jon Whittle

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

10 Citations (Scopus)


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 languageEnglish
Title of host publicationModel Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings
Number of pages15
Volume6394 LNCS
EditionPART 1
Publication statusPublished - 2010
Externally publishedYes
EventACM/IEEE International Conference on Model Driven Engineering Languages and Systems 2010 - Oslo, Norway
Duration: 3 Oct 20108 Oct 2010
Conference number: 13th (Proceedings)

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
NumberPART 1
Volume6394 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349


ConferenceACM/IEEE International Conference on Model Driven Engineering Languages and Systems 2010
Abbreviated titleMoDELS 2010
Internet address

Cite this