Towards the Formal Verification of SysML Specifications: Translation of Activity Diagrams into Modular Petri Nets

The SysML Activity diagram can be used to describe the behavior of complex systems which integrate an increasing number of components and a variety of technologies. Call behavior actions are SysML activity diagram elements used for structuring, composing and reusing activities. However, when designing complex and critical systems, the use of formal methods is strongly recommended for their validation, but the SysML language lacks formal semantics to achieve behavioral requirement verification. The present paper proposes a model-to-model transformation of SysML activity diagrams into modular Petri nets. We want to preserve the compositional structure of SysML activity diagrams in the derived Petri nets for enabling their modular and incremental verification.