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

Lukman Ab. Rahim; Jon Whittle

doi:10.1007/978-3-642-16145-2_12

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

Lukman Ab. Rahim
, Jon Whittle

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

12 Citations (Scopus)

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	https://doi.org/10.1007/978-3-642-16145-2_12
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	https://dl.acm.org/doi/proceedings/10.5555/1926458 (Proceedings)

Access to Document

10.1007/978-3-642-16145-2_12

Cite this

Ab. Rahim, L., & Whittle, J. (2010). Verifying semantic conformance of state machine-to-Java code generators. In Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings (PART 1 ed., Vol. 6394 LNCS, pp. 166-180). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6394 LNCS, No. PART 1). https://doi.org/10.1007/978-3-642-16145-2_12

Ab. Rahim, Lukman ; Whittle, Jon. / Verifying semantic conformance of state machine-to-Java code generators. Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings. Vol. 6394 LNCS PART 1. ed. 2010. pp. 166-180 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); PART 1).

@inproceedings{6e087387ce90413c88f823636ee23002,

title = "Verifying semantic conformance of state machine-to-Java code generators",

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.",

author = "Lukman Ab. Rahim and Jon Whittle",

year = "2010",

doi = "10.1007/978-3-642-16145-2\_12",

language = "English",

isbn = "3642161448",

volume = "6394 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

number = "PART 1",

pages = "166--180",

booktitle = "Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings",

edition = "PART 1",

note = "ACM/IEEE International Conference on Model Driven Engineering Languages and Systems 2010, MoDELS 2010 ; Conference date: 03-10-2010 Through 08-10-2010",

url = "https://dl.acm.org/doi/proceedings/10.5555/1926458",

}

Ab. Rahim, L & Whittle, J 2010, Verifying semantic conformance of state machine-to-Java code generators. in Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings. PART 1 edn, vol. 6394 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), no. PART 1, vol. 6394 LNCS, pp. 166-180, ACM/IEEE International Conference on Model Driven Engineering Languages and Systems 2010, Oslo, Norway, 3/10/10. https://doi.org/10.1007/978-3-642-16145-2_12

Verifying semantic conformance of state machine-to-Java code generators. / Ab. Rahim, Lukman; Whittle, Jon.
Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings. Vol. 6394 LNCS PART 1. ed. 2010. p. 166-180 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6394 LNCS, No. PART 1).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

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

AU - Ab. Rahim, Lukman

AU - Whittle, Jon

N1 - Conference code: 13th

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/78349278915

U2 - 10.1007/978-3-642-16145-2_12

DO - 10.1007/978-3-642-16145-2_12

M3 - Conference Paper

AN - SCOPUS:78349278915

SN - 3642161448

SN - 9783642161445

VL - 6394 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 166

EP - 180

BT - Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings

T2 - ACM/IEEE International Conference on Model Driven Engineering Languages and Systems 2010

Y2 - 3 October 2010 through 8 October 2010

ER -

Ab. Rahim L, Whittle J. Verifying semantic conformance of state machine-to-Java code generators. In Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Proceedings. PART 1 ed. Vol. 6394 LNCS. 2010. p. 166-180. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); PART 1). doi: 10.1007/978-3-642-16145-2_12

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this