SysML State Machine Diagra m to Si m ple Pro m ela Verification Model Translation Method

In this study, we developed a method for converting SysML state machine diagrams into Promela models that can be verified using the SPIN model checking tool. The Promela code generated in our approach is a sequential verification model that simplifies the verification process when used in the early stages, and also prevents state explosion in the verification process. Thus, using the sequential verification model reduces the cost of the overall verification process. In this paper, we describe the rules used to convert the SysML state machine diagrams with parallel processes to a single sequential process in Promela.