Yufei Yin^1,2 Shaoying Liu¹ and Yixiang Chen², ¹Hosei University, Japan and ²East China Normal University, China

SysML activity diagrams are often used as models for software systems and its correctness is likely to significantly affect the reliability of the implementation. However, how to effectively verify the correctness of SysML diagrams still remains a challenge. In this paper, we propose a testing-based formal verification (TBFV) approach to the verification of SysML diagrams, called TBFV-M, by creatively applying the existing TBFV approach for code verification. We describe the principle of TBFV-M and present a case study to demonstrate its feasibility and usability. Finally, we conclude the paper and point out future research directions.

SysML activity diagrams, TBFV, test path generation, formal verification of SysML diagram