A formal verification framework for SysML activity diagrams

• We propose a formal verification framework for complex systems.
• These systems are modeled as a composition of a set of SysML activity diagrams.
• The composition is formalized and automatically transformed into the probabilistic model checker “PRISM” input language.
• The soundness of the proposed framework is proved.
• The proposed framework verifies two real systems: the shopping online system, and the real time streaming protocol.

SysML activity diagrams are OMG/INCOSE standard diagrams used for modeling and specifying probabilistic systems. They support systems composition by call behavior and send/receive artifacts. For verification, the existing approaches dedicated to these diagrams are limited to a restricted set of artifacts. In this paper, we propose a formal verification framework for these diagrams that supports the most important artifacts. It is based on mapping a composition of SysML activity diagrams to the input language of the probabilistic symbolic model checker called “PRISM”. To prove the soundness of our mapping approach, we capture the underlying semantics of both the SysML activity diagrams and their generated PRISM code. We found that the probabilistic equivalence relation between both semantics preserve the satisfaction of the system requirements. Finally, we demonstrate the effectiveness of our approach by presenting real case studies.