Translating UML2 Activity Diagrams to Petri Nets
Dirk Fahland. Translating UML2 Activity Diagrams to Petri Nets for analyzing IBM WebSphere Business Modeler process models. Informatik-Berichte 226, Humboldt-Universität zu Berlin, 2008.
Authors
Dirk Fahland1)
Abstract
We present a formal semantics for a variant of UML2 Activity Diagrams that is used in the IBM WebSphere Business Modeler for modeling business processes. Business process models created in the IBM WebSphere Business Modeler or with other UML2 modeling tools often constitutes one of the key specification artifacts for building an information system that implements or supports the specified processes. As UML2 Activity Diagrams lack a universally agreed semantics, the step from specification to implementation usually faces a semantical impedance caused by different interpretation of the same diagram. A well-defined formal semantics for the specification language determines the interpretation of a diagram and allows for reasoning about as well as validating and verifying a given specification on common (formal) grounds.
We adapt approaches for formalizing semantics of UML2 Activity Diagrams and apply them to the core features of the IBM WebSphere Business Modeler language for purpose of formal verification. We provide a parameterized Petri net pattern for each language concepts. A diagram is translated by instantiating a pattern for each use of a concept; merging the resulting Petri net fragments according to the structure of the original diagram yields a Petri net that specifies the behavioral semantics of the diagram. The resulting Petri net can be verified for control-flow errors using the model checker LoLA. The semantics has been implemented in a tool that is available at UML2oWFN/.
Referenced Tools
UML2oWFN (which implements the formal UML2 semantics)
LoLA: A Low Level Petri Net Analyzer (which can be used for analyzing UML2 Activity Diagrams)
their combined use is described in the UML2oWFN-LoLA Tool Chain
BibTex
@TECHREPORT{Fahland_2008_uml,
author = {Fahland, Dirk},
title = {Translating {UML2 Activity Diagrams} to {Petri} Nets for analyzing {IBM WebSphere Business Modeler} process models},
institution = {Humboldt-Universit\"{a}t zu Berlin},
year = {2008},
type = {Informatik-Berichte},
number = {226},
pdf = {http://www.informatik.hu-berlin.de/~fahland/docs/fahland08_umlpn_tr_226.pdf}
}
1) Humboldt-Universität zu Berlin, Institut für Informatik, Unter den Linden 6, 10099 Berlin