Home > Research > Publications & Outputs > Verifying semantic conformance of state machine...
View graph of relations

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

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Publication date2010
Host publicationModel Driven Engineering Languages and Systems 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I
EditorsDorina C. Petriu , Nicolas Rouquette , Øystein Haugen
Place of PublicationBerlin
PublisherSpringer Verlag
Pages166-180
Number of pages15
ISBN (print)978-3-642-16144-5
<mark>Original language</mark>English

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6394
ISSN (Print)0302-9743
ISSN (electronic)1611-3349

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.