QVT Based Model Transformation from Sequence Diagram to CSP
L. Dan. Engineering of Complex Computer Systems (ICECCS), 2010 15th IEEE International Conference on, page 349 --354. (March 2010)
DOI: 10.1109/ICECCS.2010.47
Abstract
In a model driven software development paradigm, UML sequence diagrams are used for modeling the interaction view of the software. For an application with high demanding of dependability, formal verification and analysis need to be performed on the sequence diagrams. This is usually done by transforming the sequence diagrams to a well studied formalism that has effective tool support to verification and analysis. In this paper, we propose an approach for transformations from sequence diagrams to CSP processes. The transformations are implemented by using the model driven software engineering standards, such as MOF, QVT, and XSLT. For this, we design the metamodels for sequence diagrams and CSP, and a set of transformation rules are specified using the QVT graphical syntax. The transformation rules are implemented as XSLT rule-based style templates. An XSLT engine reads the XMI file of a sequence diagram produced by an UML CASE tool, and then executes the XSLT templates, outputs the CSP model as an XML file. The XML file of the CSP processes can be translated into the input of a CSP checker for verification.
%0 Conference Paper
%1 dan_qvt_2010
%A Dan, Li
%B Engineering of Complex Computer Systems (ICECCS), 2010 15th IEEE International Conference on
%D 2010
%K , Language; Model, QVT}, Software, UML}, Unified}, XMI}, XSLT}, based, communicating, development, driven, engineering; formal, graphical, model, modeling, paradigm; processes; query-view-transformation, rule-based, sequence, sequential, software style, templates; verification; {CASE}, {MOF; {diagrams; {engine; {file; {syntax; {tool; {transformation;
%P 349 --354
%R 10.1109/ICECCS.2010.47
%T QVT Based Model Transformation from Sequence Diagram to CSP
%X In a model driven software development paradigm, UML sequence diagrams are used for modeling the interaction view of the software. For an application with high demanding of dependability, formal verification and analysis need to be performed on the sequence diagrams. This is usually done by transforming the sequence diagrams to a well studied formalism that has effective tool support to verification and analysis. In this paper, we propose an approach for transformations from sequence diagrams to CSP processes. The transformations are implemented by using the model driven software engineering standards, such as MOF, QVT, and XSLT. For this, we design the metamodels for sequence diagrams and CSP, and a set of transformation rules are specified using the QVT graphical syntax. The transformation rules are implemented as XSLT rule-based style templates. An XSLT engine reads the XMI file of a sequence diagram produced by an UML CASE tool, and then executes the XSLT templates, outputs the CSP model as an XML file. The XML file of the CSP processes can be translated into the input of a CSP checker for verification.
@inproceedings{dan_qvt_2010,
abstract = {In a model driven software development paradigm, {UML} sequence diagrams are used for modeling the interaction view of the software. For an application with high demanding of dependability, formal verification and analysis need to be performed on the sequence diagrams. This is usually done by transforming the sequence diagrams to a well studied formalism that has effective tool support to verification and analysis. In this paper, we propose an approach for transformations from sequence diagrams to {CSP} processes. The transformations are implemented by using the model driven software engineering standards, such as {MOF}, {QVT}, and {XSLT.} For this, we design the metamodels for sequence diagrams and {CSP}, and a set of transformation rules are specified using the {QVT} graphical syntax. The transformation rules are implemented as {XSLT} rule-based style templates. An {XSLT} engine reads the {XMI} file of a sequence diagram produced by an {UML} {CASE} tool, and then executes the {XSLT} templates, outputs the {CSP} model as an {XML} file. The {XML} file of the {CSP} processes can be translated into the input of a {CSP} checker for verification.},
added-at = {2013-02-28T11:13:35.000+0100},
author = {Dan, Li},
biburl = {https://www.bibsonomy.org/bibtex/224a9c34cfe062e1d64157dd715b14efd/fritzsolms},
booktitle = {{Engineering of Complex Computer Systems {(ICECCS)}, 2010 15th {IEEE} International Conference on}},
doi = {10.1109/ICECCS.2010.47},
interhash = {46d705407eb2deb15b3b299a99417e29},
intrahash = {24a9c34cfe062e1d64157dd715b14efd},
keywords = {, Language; Model, QVT}, Software, UML}, Unified}, XMI}, XSLT}, based, communicating, development, driven, engineering; formal, graphical, model, modeling, paradigm; processes; query-view-transformation, rule-based, sequence, sequential, software style, templates; verification; {CASE}, {MOF; {diagrams; {engine; {file; {syntax; {tool; {transformation;},
lccn = {0000},
month = mar,
pages = {349 --354},
timestamp = {2013-02-28T11:13:44.000+0100},
title = {{{QVT} Based Model Transformation from Sequence Diagram to {CSP}}},
year = 2010
}