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.