Abstract

"Model-Based Systems Engineering (MBSE) has been utilized in the design and behavioral modeling of cyber-physical systems. The Vee model helps frame MBSE's lifecycle approach, with system verification a vital aspect of the qualification process. However, popular modeling language tools in MBSE, such as Systems Modeling Language (SysML), are incapable of formally verifying these systems. In addressing this shortcoming, model checking can be looked upon since it allows for the development of formal system models similar in abstraction to SysML models towards automatically checking if these formal models satisfy formal specifications. In the paper, we proposed an approach to translate behavioral diagrams in SysML, such as state-machine diagrams, to the popular symbolic model checker NuSMV for formal verification. As a case study, we applied this process to autonomous multi-differential drive robots (DDR). Subsequently, the NuSMV model is verified against some formal operational specifications obtained from the requirements diagram of the DDR. This system verification approach can help System Engineers identify design flaws or incorrect modeling or specifications that could be missed during the design phase through the results of the model checking process."