학술논문

Verifying SysML activity diagrams using formal transformation to Petri nets
Document Type
redif-article
Source
John Wiley & Sons, Systems Engineering. 23(1):118-135
Subject
Language
English
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.