Standard
Verifying semantic conformance of state machine-to-java code generators. / Rahim, Lukman Ab
; Whittle, Jon.
Model Driven Engineering Languages and Systems 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I. ed. / Dorina C. Petriu ; Nicolas Rouquette ; Øystein Haugen. Berlin: Springer Verlag, 2010. p. 166-180 (Lecture Notes in Computer Science; Vol. 6394).
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Rahim, LA
& Whittle, J 2010,
Verifying semantic conformance of state machine-to-java code generators. in DC Petriu , N Rouquette & Ø Haugen (eds),
Model Driven Engineering Languages and Systems 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I. Lecture Notes in Computer Science, vol. 6394, Springer Verlag, Berlin, pp. 166-180.
https://doi.org/10.1007/978-3-642-16145-2_12APA
Rahim, L. A.
, & Whittle, J. (2010).
Verifying semantic conformance of state machine-to-java code generators. In D. C. Petriu , N. Rouquette , & Ø. Haugen (Eds.),
Model Driven Engineering Languages and Systems 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I (pp. 166-180). (Lecture Notes in Computer Science; Vol. 6394). Springer Verlag.
https://doi.org/10.1007/978-3-642-16145-2_12Vancouver
Rahim LA
, Whittle J.
Verifying semantic conformance of state machine-to-java code generators. In Petriu DC, Rouquette N, Haugen Ø, editors, Model Driven Engineering Languages and Systems 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I. Berlin: Springer Verlag. 2010. p. 166-180. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-16145-2_12
Author
Rahim, Lukman Ab
; Whittle, Jon. /
Verifying semantic conformance of state machine-to-java code generators. Model Driven Engineering Languages and Systems 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I. editor / Dorina C. Petriu ; Nicolas Rouquette ; Øystein Haugen. Berlin : Springer Verlag, 2010. pp. 166-180 (Lecture Notes in Computer Science).
Bibtex
@inproceedings{cbfa080c3d924e81b6c98c4ca79f9302,
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{\textquoteright}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 = "Rahim, {Lukman Ab} and Jon Whittle",
year = "2010",
doi = "10.1007/978-3-642-16145-2_12",
language = "English",
isbn = "978-3-642-16144-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "166--180",
editor = "{Petriu }, {Dorina C.} and {Rouquette }, {Nicolas } and {\O}ystein Haugen",
booktitle = "Model Driven Engineering Languages and Systems 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I",
}
RIS
TY - GEN
T1 - Verifying semantic conformance of state machine-to-java code generators
AU - Rahim, Lukman Ab
AU - Whittle, Jon
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.
U2 - 10.1007/978-3-642-16145-2_12
DO - 10.1007/978-3-642-16145-2_12
M3 - Conference contribution/Paper
SN - 978-3-642-16144-5
T3 - Lecture Notes in Computer Science
SP - 166
EP - 180
BT - Model Driven Engineering Languages and Systems 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I
A2 - Petriu , Dorina C.
A2 - Rouquette , Nicolas
A2 - Haugen, Øystein
PB - Springer Verlag
CY - Berlin
ER -
