Recursive ECATNets-Based Approach for Formally Verifying SysML Activity Diagrams

International audienceSystem Modelling Language (SysML) is a modelling language that allows system description with various integrated diagrams. The SysML activity diagram (SAD) is widely used to graphically describe system behaviours. Nevertheless, despite the various advantages of SysML, it lacks for formal semantics to achieve the verification of behavioural requirements. Petri nets (PNs) are a popular technique for modelling and verifying the dynamic behaviours of systems. Recursive ECATNets (RECATNets) not only take all the advantages of PNs but also allow concise specifications and more capabilities for the verification process. In this study, the authors propose an approach which describes a verification methodology of SADs based on their transformation into RECATNet models. Case studies are presented to show the benefits and the usefulness of the proposed approach