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.