Towards a Fractionation-based Verification: Application on SysML Activity Diagrams

This work contributes to reduce the cost of the verification process of model-based systems, especially the ones designed as SysML activity diagrams, by relying on the concept of diagram calls defined in SysML standard. By exploiting the diagram calls concept, we propose a mechanism to transform a given diagram into its equivalent fractal (hierarchical) form. Further, we present an abstraction algorithm to reduce the size of the obtained SysML activity diagram by ignoring the irrelevant behaviors and by merging similar artifacts. To do verification, the abstracted diagram is transformed automatically into PRISM source code to check the system’s requirements that are specified in the probabilistic temporal logic, PCTL. The soundness of the provided framework is presented for each step, and, its practical effectiveness is demonstrated on diagrams obtained by reversing the open source of OpenSAF middle-ware.