Formal Extension and Verification of System Design Models for Complex Mechatronic Systems Based on SysML

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.