Towards a Call Behavior-Based Compositional Verification Framework for SysML Activity Diagrams

SysML activity diagram is a standard modeling language for complex
systems. It supports systems’ composition by providing the operator ‘call
behavior’. In general, the verification of systems modeled with those diagram inherit
the limitations of the developed built-in tools, especially the case of model
checking. To address this shortcoming, we propose a compositional verification
framework based on the call behavior operator to alleviate the state space explosion
problem of model-checking. The framework decomposes a property into
local sub-properties and verify them separately on the composed behavioral diagrams.
Further, we propose to ignore the diagrams artifacts that are useless with
respect to the property under verification. We prove the soundness of the proposed
approach by showing that the result deduced from the verification of the
local properties is always preserved. The verification results are obtained by encoding
SysML activity diagrams in the probabilistic model checker ‘PRISM’.
Finally, we demonstrate the effectiveness of our framework by verifying a set of
properties on two use cases that require a large amount of memory and a considerable
time processing.