Petri Nets Based Approach for Modular Verification of SysML Requirements on Activity Diagrams.
Messaoud Rahim, Malika Ioualalen, Ahmed Hammad · 2014
Abstract. The validation of SysML specifications needs a complete process for extracting, formalizing and verifying SysML requirements. Within an overall approach which considers an automatic verification of SysML designs by translating both requirement and behavioral diagrams, this paper proposes a modular verification of SysML functional require-ments on activity diagrams. The contribution of this paper is the proposi-tion of a methodology guided by the relationships between requirements and SysML activities for verifying complex systems with many compo-nents. We propose a model-to-model transformation to automatically derive from SysML activities a modular Petri net, then SysML require-ments are formalized and verified using the derived Petri net modules. A case study is presented to demonstrate the effectiveness of the proposed approach.