Verifying SysML activity diagrams using formal transformation to Petri nets. Issue 1 (12th November 2019)

• Record Type: Journal Article
• Authors: Huang, Edward; McGinnis, Leon F.; Mitchell, Steven W.
• Is Part Of: Systems engineering. Volume 23:Issue 1(2020)
• Page Start: 118
• Page End: 135
• Publication Date: 2019-11-12
• Subjects: model‐based systems engineering -- system behavior modeling -- model transformation; Systems engineering -- Periodicals; 620.0011
• DOI: 10.1002/sys.21524
• Languages: English
• ISSNs: 1098-1241

Abstract

Abstract: The development of contemporary systems is an extremely complex process. One approach to modeling system behavior uses activity diagrams from Unified Modeling Language (UML)/System Modeling Language (SysML), providing a standard object‐oriented graphical notation and enhancing reusability. However, UML/SysML activity diagrams do not directly support the kind of analysis needed to verify the system behavior, such as might be available with a Petri net (PN) model. We show that a behavior model represented by a set of fUML‐compliant modeling elements in UML/SysML activity diagrams can be transformed into an equivalent PN, so that the analysis capability of PN can be applied. We define a formal mathematical notation for a set of modeling elements in activity diagrams, show the mapping rules between PN and activity diagrams, and propose a formal transformation algorithm. Two example system behavior models represented by UML/SysML activity diagrams are used for illustration.