Efficient Probabilistic Abstraction for SysML Activity Diagrams

SysML activity diagrams are OMG/INCOSE standard models for specifying and analyzing systems’ behaviors. In this paper, we propose an abstraction approach for this type of diagrams that helps to mitigate the state-explosion problem in probabilistic model checking. To this end, we present two algorithms to reduce the size of a given SysML activity diagram. The first eliminates the irrelevant behaviors regarding the property under check, while the second merges control nodes into equivalent ones. The resulting abstracted model can answer safely the Probabilistic Computation Tree Logic (PCTL) property. Moreover, we present a novel calculus for activity diagrams (NuAC) that captures their underlying semantics. In addition, we prove the soundness of our approach by defining a probabilistic weak simulation relation between the semantics of the abstract and the concrete models. This relation is shown to preserve the satisfaction of the PCTL properties. Finally, we demonstrate the effectiveness of our approach on an online shopping system case study.