Abstract: Formal system verification is an important method to guarantee the correctness of system design.Because of the physical-software synergetic characteristics of complex mechatronic systems,how to verify the system design from the dynamic perspective is a challenging issue in this research area.To this end,we proposed a formal system model verification method by extending SysML,which is the standard modeling language for systems engineering.Specifically,first,we combined the computational tree logic(CTL)and flow-based functional representation as the formal basis and proposed a system functional modeling method in SysML;then,we proposed a system behavioral modeling method in SysML based on hybrid automata(HA);finally,specific to the different dynamics of physical and software subsystems,we conducted the system design model verification in a layered manner by leveraging the model checker NuSMV.We used the mobile robot system as a case study to illustrate the system verification process.