Formal Verification Of SysML State Machine: Timed Automata Approach

SysML state machine(SysML-STM)is a modeling tool used in the Systems Modeling Language(SysML)to describe the behavior of a system.It is widely used in model-driven development(MDD).Formal methods are mathematical techniques to ensure the correctness,reliability and safety of software systems and hardware designs.In this paper,we introduce formal methods in to MDD by transforming a SysML-STM model into a Uppaal timed automata.By formally verifying the system at an early stage of the system at an early stage of the development life-cycle,we aim to enhance the system’s robustness.We propose a mapping rules between the two models and have developed tools to transform them directly.Our approach enables us to effectively leverage the benefits of formal verification techniques to ensure the correctness and reliability of the system.And the direct transformation of these models not only reduces the learning cost for developers but also helps to promote the wider adoption of formal methods.In this paper,our main contributions are:· We propose mapping rules to transform SysML-STM models into Uppaal timed automata.Element mapping is performed for common elements of SysML state machine diagrams,which are mapped to elements in the Uppaal time automata.To ensure semantic consistency of the model transformation,the definition of the source model elements is considered in element mapping,and the same semantic elements in the target model are used to complete the mapping.· Based on the definitions of SysML state machine graph(source model)and Uppaal time automata(target model),metamodels of SysML state machine graph and Uppaal model were designed,the two metamodels were described using the Ecore model,and an automatic transformation tool was developed using the ATL model transformation language.· We demonstrate the effectiveness and feasibility of our approach by using two case studies,“Soldiers cross the river” and “Time Sensitive Networking”,to showcase the integration of SysML-STM modeling,transforming into Uppaal,and formal verification.