Open AccessArticle

A Model Transformation Method Based on Simulink/Stateflow for Validation of UML Statechart Diagrams

Runfang Wu

^1,2

Ye Du

^1,2,*

and

Meihong Li

^1,2

Cyberspace Security Department, School of Cyberspace Science and Technology, Beijing Jiaotong University, No. 3 Shangyuancun Haidian District, Beijing 100044, China

Tangshan Research Institute of Beijing Jiaotong University, No. 46 Xinhua West Road, Lunan District, Tangshan 063000, China

Author to whom correspondence should be addressed.

Mathematics 2025, 13(5), 724; https://doi.org/10.3390/math13050724

Submission received: 15 January 2025 / Revised: 10 February 2025 / Accepted: 19 February 2025 / Published: 24 February 2025

(This article belongs to the Special Issue Formal Methods in Computer Science: Theory and Applications)

Download

Browse Figures

Figure 1
The overall process of model-driven architecture. "> Figure 2
Framework diagram of model detection knowledge logic. "> Figure 3
Schematic diagram of real-time system formal verification. "> Figure 4
Decomposing a language into a syntax tree (AST). "> Figure 5
Process of model transform from Stateflow to SMV. "> Figure 6
Performing lexical and grammatical analysis on information through ANTLR. "> Figure 7
Converting based on a complete NuSMV specification template. "> Figure 8
State diagram of railway section route algorithm. "> Figure 9
Example of partial element transformation in the model. "> Figure 10
State diagram of railway turnout state transition. "> Figure 11
State diagram of railway turnout state transition. "> Figure 12
State Diagram of Railway Turnout State Transition. The red information flow shows thecomplete link from the initial state to the successful route determination. "> Figure 13
State diagram of railway turnout state transition. The red information flow shows thecomplete link from the initial state to the routeNotFound determination. "> Figure 14
State diagram of railway turnout state transition. ">

Versions Notes

Abstract

A model transformation method based on state refinement and semantic mapping is proposed to address the challenges of high modeling complexity and resource consumption in symbolic validation of industrial software requirements. First, a rule-based semantic mapping system is constructed through the explicit definition of element correspondence between statechart components and verification models, coupled with a composite state-level refinement strategy to structurally optimize model hierarchy. Second, an automated transformation algorithm is developed to bridge graphical modeling tools with formal verification environments, supported by quantitative evaluation metrics for mapping validity. To demonstrate its practical applicability, the methodology is systematically applied to railway infrastructure safety—specifically the railroad turnout control system—as a critical case study. The experimental implementation converts operational statecharts of turnout control logic into optimized NuSMV models. Not only did the models remain intact, but the state space was also effectively reduced through the optimization of the hierarchical structure. In the validation phase, the converted model is tested for robustness using the fault injection method, and boundary condition anomalies that are not explicitly stated in the requirement specification are successfully detected. The experimental results show that the validation model generated by this method has improved validation efficiency in the NuSMV tool, which is significantly better than the traditional conversion method.

Keywords:

software model checking; formal verification; UML state diagram; model transformation

MSC:

68Q45

1. Introduction

UML (unified modeling language), a standardized modeling language, provides a clear, structured way to represent system states and transitions. In industrial system development, UML state machine diagrams are an ideal tool for the system analysis and design phase due to their intuitive and visual nature. They help developers quickly understand system behavior and facilitate effective communication between teams. UML state machine diagrams are suitable for modeling real-time systems, especially in scenarios involving multiple states, concurrent processing, and event response. They provide a clear representation of the behavior of complex systems by describing the individual states of the system, state transfers, and their triggering conditions [1]. In addition, the hierarchical structure of state machine diagrams makes it easier to modify and extend the system, and can flexibly respond to the challenges brought about by changes in system requirements. Therefore, UML state machine diagrams have significant advantages in industrial system development and are widely used in system design and analysis.

To ensure that the design and implementation process of a test system conforms to established standards, developers should consolidate the reliability of the system by validating the state machine model to better support real-time response and parallel interactive operations. However, the standard UML state machine has certain limitations that can easily lead to discrepancies between the model and the actual implementation. This discrepancy is mainly reflected in the following two aspects, the first being semantic ambiguity. The UML specification fails to explicitly define key details such as state migration priorities [2] and event handling mechanisms. For example, in a rail transit signaling system, when multiple concurrent events (e.g., train approach signals and track occupancy detection) are triggered at the same time, different tools may interpret the state transfer order differently, thus triggering inconsistent behaviors. The discrepancy is also reflected in validation faults. Traditional UML-based test case generation usually relies on manual derivation (e.g., module structure diagrams), which makes it difficult to cover complex timing logic. This deficiency often needs to be remedied at a later stage to prevent potential faults (in the case of the Boeing 787 avionics system, for example, the communication bus was blocked due to undetected state machine deadlocks in its early design, which was eventually resolved only through additional testing by a formal verification tool, which has greatly inspired this study). Therefore, the limitations of state machines need to be compensated by more precise semantic definitions and formal verification methods.

Therefore, symbolic model verification techniques based on model-driven architectures have been incorporated into the field to optimize the verification process. MDA automates the transformation from high-level design models to code through three layers of abstraction (CIM, PIM, and PSM) and is capable of automatically performing quantitative and repetitive verification of system functional attributes. To date, a series of verification tools has been developed based on the real-time systems approach, such as NuSMV [3,4], SPIN [5,6,7], and UPPAAL [8,9], which are particularly suitable for the verification of dynamic real-time systems such as railroads and trains [10,11]. The basic process of model-driven architecture is shown in Figure 1. The core idea of MDA is to verify the relevant properties of a system by modeling the state transition diagram of the system and transforming it into an executable formal code using a model transformation technique, and provide to counterexamples in the process to help developers discover potential problems in time.

Existing formalization tools show significant differentiation in real-time system verification, and we give some examples (shown in Table 1). Although they have been successfully applied in several domains, they still face some challenges in practical applications, especially the problem of model transformation faults. For example, while developing the French TGV signaling system, Alstom found that it needed to invest a significant amount of time in correcting manual conversion errors from UML models to NuSMV. This issue highlights a key challenge in the field: the need for a complete, standardized modeling and conversion process to ensure that validation models can effectively correspond to the actual system and that consistency is maintained.

Based on this requirement, we propose a system modeling and verification methodology. The idea of the approach is to use a UML state machine as a carrier of system information, and then complete the development process from system requirements analysis to validation through a model-driven architecture. Simulink/Stateflow has a clear advantage in modeling dynamic system architectures, components, and units (e.g., railroads and aeronautics) by its visual hierarchical modeling and closed-loop simulation and validation. The generated state diagrams are highly readable and rich in detail, making them more suitable for the early stages of standardized modeling. However, they lack precise semantic descriptions. Our approach converts these state charts into formal validation model (SMV) code through lexical and semantic transformation rules [12]. To demonstrate that the converted models are usable and accurate, we model the logic of some modules of a train turnout system as an example, write linear temporal logic formulas for them, and use the outputs as benchmarks to verify that the model conversions are correct.

The main contributions of this work are as follows:

Analysis and development of the unit modules of complex real-time systems to ensure their security and correctness;
Achieving a smooth transition from the logical design of Simulink state diagrams to verification and obtaining target model code suitable for verifying functional attributes;
Highly automated model transformation and coding processes.

The structure of this manuscript is as follows: Section 2 of this article introduces the basic knowledge of state machines based on UML. Section 3 provides a detailed introduction to the specific methods of model transformation, and then analyzes the correctness of the model transformation method. Section 4 verifies the effectiveness of the proposed method through examples. Section 5 summarizes the work of this article and proposes future research directions.

2. Basic Knowledge

2.1. UML State Machine Based on Simulink/Stateflow

We create a UML state machine for the following research purposes: to investigate the complexity of classes, roles, subsystems, or components within a system by describing the sequence of states experienced by objects or the interaction events that respond during their lifecycle [13].

The states, transitions, events, and activities related to objects are essential graphic elements in the Simulink/Stateflow state diagram: blocks, starting points, transitions, and connection nodes. Afterward, auxiliary program commands and function statements will be added to the diagram to complete the entire state transition process.

We will provide a detailed explanation based on the semantic elements used in the paper. Based on the state module we use, the state machine object is a collection of all state graph objects in the state flow model, and there may be inclusion/combination (or hierarchical nesting) relationships between states [14]. Therefore, state flow can use a hierarchical structure to represent the sub-components of multiple levels in the following system [15].

State. A state describes the result of executing the dynamic behavior of the object where the state machine is located. A single state has its own state name, entry/exit actions (actions executed when entering and exiting this state), and substates (if another state is nested internally, it is “Composite”; otherwise, it is “Basic”). We usually use a rounded rectangle to represent a single state on a graph. If this state is at the beginning or end of the entire lifecycle, it must be a simple state, represented by a hollow circle (or solid circle).
Transform. A transition describes the changes in the object where the state machine is located. Assuming an object is in the source state when it receives a trigger event or satisfies a guardianship condition, it will activate a transition, causing it to jump to another target state and possibly perform specific actions. On the graph, we use arrows connecting two states to represent a single transition. In addition, events, conditions, and actions are written on their associated transition paths.
Action. It is an executable atomic operation that cannot be interrupted, and its execution time can be ignored. Actions may occur within the state (executed upon entry and exit) or during transitions (executed upon completion of state transitions).

Based on these concepts, we define a Simulink-based state machine as a

S F : =

〈 S, V a r

T, t d 〉

. Among them:

S is a finite set of all states;
$V a r$ is a finite set of all variables, with data types such as $i n t 16, i n t 32, b o o l$ , etc.
$T \subseteq S \times {E v, C o n, A c t} \times S$ . It is a finite set of migrations. $E v$ is an event, $C o n$ is a constraint condition, and $A c t$ is an action. Transform can be represented as a five-tuple $t = (s_{s}, e, c, α, s_{t})$ , where $s_{s}$ is a source state, $s_{t}$ is a target state, $e \in E v, c \in C o n, α \in A c t$ ;
$t_{d} \in T$ is the default Stateflow transform pointing to the initial state.

2.2. SMV Model Based on Symbol Verification

NuSMV is a symbol model detector based on BDDs, which is constructed, re-implemented, and extended based on SMV [16,17]. It supports multiple model representations, including synchronous models, asynchronous models, and finite state machines (FSMs) directly expressed through propositional formulas. It also supports describing expected attributes as CTL, LTL, and PSL formulas.

In the design and development of a real-time system, there are often requirements such as operational flow processing, data processing, and operations between different modules (such as message passing and collaborative work [18]). These steps can be refined, characterized as individual state nodes, and connected with varying jump conditions. The entire system can be expressed using time automata. Figure 2 is a framework diagram of model detection knowledge logic.

Therefore, the question “whether the system satisfies a certain attribute” can be equivalently expressed as “whether the time automaton model satisfies a certain formula” so that real-time system temporal requirements can be visually verified by checking whether the model satisfies the corresponding formula. The core of this method lies in two aspects: first, the abstract representation of system modeling must be correct and effective, and second, the validation formula must be standardized and equivalently describe the properties to be validated.

SMV is a hierarchical model language where the semantics of each layer are contained in the module declaration, which is a set of declared constraints and specifications. An SMV model can have multiple module declarations, including primary and sub-module declarations. The combination of the main module and sub-modules can effectively describe the properties of the entire model, which can be formalized as follows:

N u S M V = m a i n_M O D U L E + s u b_M O D U L E s

Module M is a six-tuple: M = 〈INIT, VAR, TRANS, ASSIGN, FAIRNESS, SPEC〉. Among them,

I N I T

uses expressions to determine the initial state set of variables in the model;

V A R

uses expressions to specify a set of variables;

T R A N S

determines the transition relationship of the model and displays the process of transitioning from the current module state to the next state;

A S S I G N

is a set of primary operational forms of SMV, in which the model transformation of the entire system is operated; SPEC evaluates the computational tree logic CTL and linear time logic LTL specifications for SMV to determine their authenticity in finite state machine FSM. If false, a counter-example is provided. Figure 3 shows the schematic diagram of real-time system formal verification.

2.3. Principles of Syntax Parsing Based on ANTLR

ANTLR is a syntax analyzer generation tool that reads, processes, executes, and translates structured texts or programming languages [19]. The main parsing processes of ANTLR are lexical analysis, syntactic analysis, and AST (abstract grammar tree) analysis. Based on custom syntax files, through the above steps, the program can recognize and process text that conforms to syntax specifications and convert the original language text into the target language text according to conversion rules [20].

A syntax file is a specific data structure with a certain degree of universality within a range [21]. The syntax file of ANTLR consists of grammar and lexical rules, always starting with the grammar keyword and stored in the form of an extension of “. g4”. Grammar rules always start with lowercase letters and are composed of syntax statements and several rules that follow (they can directly or indirectly recursively refer to themselves). Lexical rules always start with uppercase letters and contain at least two parts of information: the type of lexical symbol (which can be used to identify lexical structure) and the text corresponding to that lexical symbol.

When we perform analysis operations using ANTLR, we use lexical and syntactic analyzers to transform and reconstruct input character sequences into statements under new language rules. The function of a lexical analyzer is to read and analyze the morphology of structured text or binary files and classify vocabulary symbols. The analyzed character sequence will be decomposed and stored as a single token. The syntax analyzer detects the correctness of these character sequences and establishes an analysis tree (AST), in which the leaf nodes serve as containers for storing lexical symbols in the stream (these leaves can be traversed to complete the reconstruction of new language statements). Figure 4 shows the decomposition of a language by the syntax tree AST.

3. Model Transform: From Simulink/Stateflow to NuSMV

In order to validate the non-formal Simulink/Stateflow model formally and achieve the automatic generation of model code, we adopted an automatic conversion method from the Stateflow model to the SMV model.

The Stateflow model is a finite state machine with a graph structure similar to the SMV state machine graph, consisting of states and transitions. Therefore, the model elements of the former and the latter can be mapped through specific rules. In terms of semantic transformation, we have established a mapping between Simulink and SMV meta-models to achieve semantic transformation (see Figure 5). In terms of syntax, we use Python 3.8 scripts to generate SMV models, where the target file for model transformation is a validation model script described in the SMV language. The specific syntax conversion depends on the XML text model. According to the syntax rules of Simulink text, SF.xml can be parsed, and the converted SMV syntax text can be generated based on the syntax conversion rules.

The Stateflow model is a finite state machine with a graph structure similar to the SMV state machine graph, consisting of elements such as state and transition. The model elements of the two can be mapped through specific rules. In terms of semantic transformation, we have established a mapping between the Simulink meta-model and the SMV meta-model to achieve semantic transformation. In terms of syntax, we use Python 3.8 scripts to generate SMV models, where the target file for model transformation is the validation model script described in the SMV language. The specific syntax conversion depends on the XML text model; according to the syntax rules of Simulink text, SF.xml can be parsed, and the converted SMV syntax text can be generated based on the syntax conversion rules(see Algorithm 1).

The Stateflow-SMV conversion rule Trans (SF) in the model conversion algorithm is 〈S, Var, T, td, Ch〉, which can also be expressed as follows: 〈S, s0, sf, V, T, CS

〉 \to 〈

S, Var, T, td, Ch〉.

Algorithm 1 Stateflow-SMV Transform

Input: Stateflow Model $S F$
Output: NuSMV Model $N M$
1:
elementArr ← SF
2:
for $e \in e l e m e n t A r r$ do
3:
SMV ← Stateflow API(E)
4:
NM.add(SMV)
5:
end for
6:
return SMV Model

3.1. Information Extraction

The Stateflow state machine model, as a visual graphical project, is stored using XML markup language. To collect the model-related information required for transformation, we must parse the XML language and extract its state and transition elements [22]. The ElementTree module in Python 3.8 is a way of processing XML data [23], which can parse state machine information files (usually stored in a [.json] file and a [.svg] file when exporting a project) into element tree objects and convert them into Python 3.8 dictionaries or lists to extract them.

Similarly, we extract graphical information from the model, distinguishing them into nodes, states, and transitions (based on their color and other attributes, where nodes are a specific graphical representation of states). For each transformation, we record the coordinates of the arrows’ starting and ending points to find the transformation connection’s source and target states. We will iteratively analyze states if there is a hierarchical nesting of states.

Algorithm 2 is a pseudocode that extracts information from the state machine model. It takes the XML model of Stateflow as input. It outputs an intermediate data file containing all information of the state machine model (including program statements, logical information, and function code). The algorithm extracts model-related program statements from the JSON file in lines 3 to 7, including traversing each element sj in the JSON object dictionary in line 4. The fifth line parses the sj element to obtain the name of the program statement and the binary value pair of the code. Add these numerical pairs to the information file in line 6. All JSON file information has been extracted in line 7. The algorithm extracts the logical relationships of model elements in the SVG file from lines 8 to 13 as follows: it traverses each node SVG in the SVG object tree in line 9; the 10th line distinguishes the type of node (whether it is a basic state, initial state, or migration); it analyzes and finds the logical relationship of nodes in line 11 (searches for the source state and target state of the transition); it adds the numerical information of the node to the information file in line 12; all SVG file information is extracted on line 13. The 14th line returns the extracted data file IDF, and the conversion is complete.

Algorithm 2 Stateflow-SMV Transform

Input: Stateflow Model $S F$
Output: Intermediate Data File $I D F$
1:
elementDicJ ← SF.json
2:
for $s j \in e l e m e n t D i c J$ do
3:
( $N a m e_{s j}$ , $C o d e_{s j}$ ) ← Extract(j)
4:
IDF.add( $N a m e_{s j}$ , $C o d e_{s j}$ )
5:
end for
6:
elementTreeSVG ← SF.SVG
7:
for $s v g \in e l e m e n t T r e e S V G$ do
8:
$C a t g_{s v g} \leftarrow$ Distinguish(svg)
9:
$L o g i c_{s v g} \leftarrow$ Check(svg)
10:
IDF.add( $C a t g_{s v g}, L o g i c_{s v g}$ )
11:
end for
12:
return IDF Data

3.2. State Refinement

Our research proposes an abstraction and refinement method based on state flow state machines to decompose complex state machine models. The proposed state machine refinement rules are divided into decomposition refinement of complex states and transformation refinement. For ease of description, the symbol ↦ is used to represent the refinement relationship,

n a m e (s)

represents the name of state s, symbol

S^{'}

represents the refined state set,

T^{'}

represents the refined transition set,

t^{'}

represents the refined transition, and

C S^{'}

represents the refined composite state.

We define a simple state in a state machine as

s = (n a m e, T_{i n}, T_{o u t}, A_{e n}, A_{e x}, A_{d o})

, where

T_{i n}

is the migration set with the target state s,

T_{o u t}

is the migration set with the source state s,

A_{e n}

is the action set executed when entering s,

A_{e x}

is the action set executed when exiting s,

A_{d o}

is the set of actions executed within state s.

We consider the hierarchical state machine model as a tree structure, with each state viewed as a node in the tree. The complex state obtained when we traverse the tree to the leaf node can be used as a refinement object. Otherwise, we continue to decompose downwards. We define a complex state

s_{c} = (P, t y p e, s u b, A, T)

in the state machine before refinement, where P is the parent node of

s_{c}

t y p e

is the type of

s_{c}

(which used to distinguish whether the state is a basic state), sub is the child node of

s_{c}

(this item is empty when s is a basic state), A is the set of actions involved in

s_{c}

, and

s_{c} . A = 〈 A_{e n}, A_{e x}, A_{d o} 〉

(including the entry action, exit action, and internal action of this state), T is the migration set involved in

s_{c o m}

s_{c} . T = 〈 T_{i n}, T_{o u t} 〉

(including all migration sets with target state

s_{c}

and source state

s_{c}

. The purpose of refinement rules is to eliminate hierarchical relationships in the state diagram and flatten all complex states into basic states.

Here are the refinement rules we follow (see Equation (1)).

r e f (S t a t e f l o w) = \frac{S^{'} = S \cup {s_{0}, s_{1}, \dots, s_{k}}, \forall n \neq m, s_{n}, s_{m} \in S^{'}, n a m e (s_{n}) \neq n a m e (s_{m})}{S \mapsto S^{'}, s \mapsto {s_{0}, s_{1}, \dots, s_{k}}}

(1)

The refinement rule represents adding multiple states

s_{0}, s_{1}, \dots s_{k}

based on the original state set, and refining the original state set S to

S^{'}

. To avoid naming conflicts, ensuring that the state names in the refined state set do not produce duplicates is necessary. The operations required to refine complex state

s_{c}

into simple state

s^{'}

are as follows (see Equation (2)).

\begin{matrix} r e f (s_{c}) = s_{c} \mapsto s^{'}, s \in {s_{0}, s_{1}, \dots, s_{k}} \\ n a m e (s^{'}) = n a m e (s_{c} \to P) \lor n a m e (s_{c}) \\ A_{e n} (s^{'}) = A_{e n} (s_{c} \to P) \land A_{d o} (s_{c} \to P) \land A_{e n} (s_{c}) \\ A_{d o} (s^{'}) = A_{d o} (s_{c}) \\ A_{e x} (s^{'}) = A_{e x} (s_{c} \to P) \land A_{e x} (s_{c}) \\ T_{i n} (s^{'}) = T_{i n} (s_{c} \to P) \land T_{i n} (s_{c}) \\ T_{o u t} (s^{'}) = T_{o u t} (s_{c}) \end{matrix}

(2)

After removing the hierarchical relationship of the state machine, all transitions to substates will be transformed into new transition relationships (see Equation (3)).

r e f (S t a t e f l o w . T) = \frac{T^{'} = T \cup {t_{1}, t_{2}, \dots, t_{j}}, \forall u \neq v, t_{u}, t_{v} \in T^{'}, r a n k (t_{u}) \neq r a n k (t_{v})}{T \mapsto T^{'}, t \mapsto {t_{1}, t_{2}, \dots, t_{j}}}

(3)

Algorithm 3 is a pseudocode that refines the state machine Stateflow, using the model information of the state machine as input. The algorithm refines each complex state in the state machine from line 4 to line 14, including traversing the state nodes in the state machine in line 4. The fifth line parses the node (complex state) element, obtaining the state name, upper-level state, state type, lower-level state, state migration, and state action. The sixth line distinguishes the type of node (whether it is the basic state of the leaf node). The status name is refined in the seventh line. The entry action, internal action, and exit action of the refinement state are obtained in line 8, the in-migration and out-migration of the refined state in line 9. The integrated simple state is added to the refined state set in the 10th line. The 11th line adds the refined migration to the new migration set, and the 14th line returns the refined state set data file IDF, indicating the end of refinement.

Algorithm 3 Refinement of Stateflow Model

Input: Stateflow Model Data File $S T D F$
Output: Data File After Refinement $D F A R$
1:
hirtreeSF ← STDF
2:
for $n o d e \in h i r t r e e S F$ do
3:
     ( $N a m e, P, t y p e, s u b, A, T$ ) ← node
4:
    if $n o d e . t y p e! = “ b a s i c ”$ then
5:
          $b a s i c_{s} . n a m e \leftarrow$ ref(node.name)
6:
          $b a s i c_{s} . (A_{e n}, A_{d o}, A_{e x}) \leftarrow$ ref(node.A)
7:
          $b a s i c_{s} . (T_{i n}, T_{o u t}) \leftarrow$ ref(node.T)
8:
         DFAR.add( $b a s i c_{s}$ )
9:
         DFAR.add(ref(node.T))
10:
   end if
11:
end for
12:
return DFAR Data

3.3. Semantic Mapping

For the convenience of differentiation, we add the prefix “

s f

” to represent the elements of Stateflow and use the prefix “

n m

” to represent the elements of NuSMV. Then, we provide a series of semantic mapping rules from Stateflow to NuSMV, as shown below. In addition, we also provide a mapping table from Matlab 2020b to SMV language in ANTLR, all of which are detailed in Appendix A.

Rule 1. Mapping of variables

T r a n s (s f_V) = n m_V a r

. Among them,

s f_V

is the variable set of the state model, and

n m_V a r

is the set of the validation model. The data types of state machines include logical (true or false), integer (int32/unit32), and floating point number (single, double), which correspond to Boolean, integer, and signed/unsigned fonts in the validation model through semantic mapping operations. The type “String” is converted to the corresponding string type, as shown in conversion rules 1 to 3 (see Table 1).

Rule 2. Mapping of simple states

T r a n s (s f_s) = n m_S

. Among them,

s f_s

is a single basic state in the state model, and

n m_S

is the individual state of the validation model. For a single basic state, the expression of Stateflow and SMV is consistent and can be directly mapped, as shown in transition rule 4 (see Table 1).

T r a n s (s f_i n i s) = n m_s 0

. Among them,

s f_i n i s

is the initial state in the state model, and

n m_{s} 0

is the initial state in the validation model. Through semantic mapping operations, we map the initial state elements in Stateflow to the initial state elements in SMV. If there is no initial state in the Stateflow, the initial activity state of the model pointed to by the default migration will be taken as the initial state and mapped to the initial state element

n m_{s} 0

in SMV, as shown in conversion rule 5 (see Table 1).

T r a n s (s f_f i n s) = n m_s f

. Among them,

n m_s f

is the final state in the SMV model. There is no final state in StateFlow, but a state without migration can indicate the end of the state machine. Therefore, through semantic mapping operations, we map the state of the non-output transfer edge to the basic state of SMV, as shown in transition rule 6 (see Table 1).

Rule 3. Migration mapping

T r a n s (s f_T) = n m_T

. Among them,

s f_T

is the transition in the state model,

n m_T

is the transfer in the validation model, and the transfer in the Stateflow state machine and SMV time automaton both represent state transitions that can be directly mapped while maintaining the corresponding source and target states, i.e.,

s f_s s = T r a n s (s f_s s) & s f_s t = T r a n s (s t_s t)

, as shown in conversion rule 7 (see Table 2).

T r a n s (s f_E v) = n m_C o n d

. Among them,

s f_E v

is an event in the state model,

n m_C o n d

is the constraint condition in the validation model. Event

s f_E v

migration can only be executed when

E v

occurs; Boolean expression

n m_C o n d

also determines the conditions for migration execution. Therefore,

s f_E v

on migration mapped to

n m_C o n d

, as shown in conversion rule 8 (see Table 2).

T r a n s (s f_G) = n m_C o n s

. Among them,

s f_G

is the guard condition in the state model, and

n m_C o n s

is the constraint condition in the validation model. The guarding conditions are

s f_G

and condition

n m_C o n s

is a Boolean expression determining whether a decision transfer can be executed. We transform

s f_G

mapping through semantic mapping operations to

n m_C o n s

, as shown in conversion rule 9 (see Table 2).

T r a n s (s f_A c t) = n m_A c t

. Among them,

S f_A c t

is the action executed during Stateflow state migration, which can be mapped to the program action executed during SMV migration, as shown in transition rule 10 (see Table 2).

Rule 4. Matching of Constants

F l a t (s f_C o n s t a n t) = n m_C o n s t a n t E x p r e s s i o n

. The constant in state machine language is matched to the initial constant expression in SMV. The constant types in state machine language include numeric

C O N S T A N T

I N D E N T I F I E R

, and

a r r a y_l i s t

(including empty arrays), which are matched to the numerical

i n t e g e r

, symbol

w o r d

, and

a r r a y

of SMV constant expressions. It is worth emphasizing that in SMV, an enumeration type is used to represent a range of values, and all string variable values of our state variables,

S T R I N G_L I T E R A L

, can be attributed to it, which requires some detailed transformation. In addition, before declaring a state variable, SMV needs to declare a constant to fix the range of the state variable.

Rule 5. Matching of Expressions

F l a t (s f_P r i m a r y E x p r e s s i o n) = n m_B a s i c E x p r e s s i o n

. The basic expression in state machine language corresponds to matching the basic expression in SMV. The expression types of state machine language include

r e l a t i o n a l_e x p r e s s i o n

e q u a l i t y_e x p r e s s i o n

a s s i g n m e n t_e x p r e s s i o n

u n a r y_e x p r e s s i o n

b i n a r y_e x p r e s s i o n

(including addition, subtraction, multiplication, division, left division, matrix multiplication), etc., which are matched to the (

b a s i c_e x p r

) type in SMV expressions (basic expressions) and are associated with the corresponding operator (operator).

Rule 6. Matching of statements

F l a t (s t a t e m e n t) = n m_C o n s t a n t E x p r e s s i o n

. The program statement segments in state machine languages correspond to the basic operation forms in SMV. The statement types in state machine language include

a s s i g n_s t a t e m e n t

s e l e c t i o n_s t a t e m e n t

, and

e l s e i f_c l a u s e

, which are matched to the

A S S I G N C o n s t r a i n t

C a s e E x p r e s s i o n s

, and

I f - T h e n - E l s e E x p r e s s i o n s

in the basic operation form of SMV.

F l a t (f u n c t i o n_d e c l a r e) = n m_M o d u l e D e c l a r a t i o n s

. The function statement segments in state machine languages match with function declarations in SMV.

Based on the above model conversion strategy, we have summarized the conversion rules from Simulink/Stateflow to SMV (see Table 2).

3.4. Grammar Conversion

In order to convert the Simulink/Stateflow model into an SMV formal validation model, we adopted an automated conversion method to ensure semantic consistency. Firstly, we recursively traversed the AST and constructed a global symbol table, recording the hierarchical relationship of states, migration conditions, and metadata of states, events, and variables. Next, we used the encode_state() function to flatten the state and generate a unique identifier. Then, the migration logic was standardized through conversion functions by converting operators and conditions into formats supported by NuSMV and generating TRANS rules. Finally, actions and events were mapped to the NuSMV model through DEFINE and ASSIGN statements to ensure an accurate representation of the action and event logic. This transformation method enables the Stateflow model to be effectively mapped to NuSMV, supporting subsequent formal validation.

We use ANTLR for lexical analysis and language compilation, which is different from the comparison process of documents. We must match two codes considering all syntax and semantic issues. The function of ANTLR as a parser and generator can be used to parse the source code of C, CPP, and other languages and the syntax of Matlab 2020b [24]. In this research work, we use lexical analyzers and syntax parsers (as well as some files such as grammar tokens, lexer tokens, Baselistener, Listener, parse tree visitor, parse tree walker, etc.) to generate a parse tree (see Figure 6). The leaf nodes in the parse tree become containers to hold each lexical symbol in the input source code expression, and the root node corresponds to the syntax rules of this expression (see Figure 6). We traverse the parse tree, access each child node, and reconstruct them into new words and sentences under the NuSMV language rules.

Algorithm 4 is a pseudocode that flattens the state machine model’s syntax, using the state machine’s data file as input. The algorithm performs language parsing and flattening operations on the model from lines 3 to 8, including reading the data file in line 3 and decomposing it into character sequences using a lexical analyzer. The fourth line uses a syntax parser to generate a syntax tree from the character sequence. From line 5 to line 7, each node statement in the syntax tree is converted to form a new language rule statement, and the new sentence is integrated into an NuSMV model. Line 9 returns the flattened NuSMV model.

Algorithm 4 Grammar Flattening of StateFlow Model

Input: Intermediate Data File $I D F$
Output: NuSMV Model $N M$
1:
Buffer ← IDF.LexerFlow
2:
GrammarTree ← Parser.Deal(Buffer)
3:
for $g t \in G r a m m a r T r e e$ do
4:
ClassInfo ← transform(gt)
5:
NM.add(ClassInfo)
6:
end for
7:
return NM

1. Lexical Rules. We have defined the basic building blocks of the state machine model through ANTLR lexical rules, which are crucial for identifying and distinguishing various components in the state flow graph. (1) STATEMACHINE, STATE, TRANSITION, EVENT define the core elements of the state machine model, such as the entire state machine, individual states, transitions between states, and events that trigger transitions. (2) ID represents identifiers, which can be used for naming states, transitions, actions, or variables within the model. These identifiers consist of letters, digits, and underscores. (3) NUMBER defines a number, which may be used as part of conditions, comparisons, or action parameters. (4) WS defines whitespace characters (such as spaces, tabs, or newlines). These lexical rules form the foundation of the grammar, ensuring that each component of the Stateflow model is correctly identified and processed in the subsequent stages of parsing and translation to SMV code.

2. Grammar Rules. We also defined how the different components of the Stateflow model are constructed and how they are interrelated throughout the system through syntax rules. The top-level rule, model, specifies that a model consists of one or more StateMachine objects, where each state machine is represented by the state machine rule. Each state machine includes a name (identifier) and state elements. The state rule defines an individual state, which can optionally have a history attribute and contains a block that defines substates, transitions, and events. The substate rule allows for the nesting of states, where a state may have its internal structure of nested substates or transitions. Transitions between states are defined using the transition rule, which specifies a condition that must be satisfied for the transition to occur (represented by an expression expr), an optional list of actions to be executed during the transition, and the target state to which the system transitions. The event rule defines events that trigger transitions, each with a name and a triggering condition. The action_list rule describes a list of actions that can be performed during transitions, where each action is represented by an identifier and may include optional arguments, defined by the arg_list rule. The expr rule encompasses various types of expressions, including logical operations (AND, OR), comparisons (equal, not equal, greater than, less than), and variable references, which are fundamental for defining the conditions for state transitions and actions. These syntax rules establish the structure and relationships of the Stateflow model elements, facilitating the parsing of state machines into a formal format suitable for verification.

3. Status Coding and Module Definition. When converting the hierarchical state structure of Stateflow into the NuSMV model, semantic equivalence mapping needs to be achieved through state flattening encoding and modular separation. This recursively traverses the nested state nodes in the AST, starting from the root state and parsing down the hierarchical relationship of each child state. When dealing with each state, a unique, globally unique state name is formed by concatenating the name of the parent state with the name of the child state. For example, if there is a parent state named Parent with a child state named Child, then these two states will be merged into a complete state name “Parent_Child”. The use of this path prefix ensures the uniqueness of each state in the entire model and effectively avoids conflicts of states with the same name. For ease of understanding, we provide a pseudocode for recursive state encoding as follows.

Function Encode_state (state: StateNode, parent_path: String = “” ) → String:
If parent_dath is empty :
full_name ← state.name
else:
full_name ← parent_path + “_” + state.name
for each substate in state.children :
child_full_name ← encode_state(substate, full_name)
return full_name

Subsequently, in modular definition, each top-level state is mapped to an independent MODULE in NuSMV, while the substates serve as enumeration values within the module. This modular structure can clearly represent the hierarchical relationships between various states and decompose complex state machines into multiple simple modules, with each module describing a state or set of states.

4. Migration logic transformation. The goal of this step is to convert the state transition conditions in AST into NuSMV’s TRANS or ASSIGN rules to ensure that the transition conditions between states are accurately represented. Firstly, it is necessary to standardize the conditional expression, which includes two main tasks. Firstly, all logical operators such as “

& &

” and “||” must be converted to the symbols “&” and “|” used by NuSMV to ensure consistency in logical operations. Secondly, special attention needs to be paid to time-dependent conditional expressions, such as after (n, sec), which represents in Stateflow that a condition must be satisfied after n seconds have passed. In order to meet the temporal logic requirements of NuSMV, these expressions are transformed into F [n] in LTL (Linear Temporal Logic), indicating that this condition must be met in the next n steps. When binding migration targets, the target state needs to be mapped to the state name encoded in the NuSMV model to ensure that each migration target in the state machine is consistent with the corresponding state name in NuSMV. When migration involves events, such as “Event [bond]”, the condition triggered by the event will be defined as “event_trigger := cond”. This ensures that the event-triggering conditions can be correctly referenced in the NuSMV model. Ultimately, through this transformation, the migration logic can be accurately mapped to NuSMV’s TRANS rules, ensuring that the system’s behavior conforms to expectations. The corresponding SMV format template for conversion is shown in Figure 7.

In the transition between action and event handling, we map actions (such as function calls) and events (such as event triggers) in Stateflow to DEFINE or ASSIGN statements in NuSMV. The process of action transformation usually involves converting the parameters of the action into Boolean expressions or variable assignments that NuSMV can understand. In this way, the action logic in Stateflow can be expressed in NuSMV.

The grammar conversion process has the following characteristics and advantages. First, the process follows a hierarchical and progressive structure, starting from lexical analysis and proceeding through syntax parsing, state flattening, and transition logic conversion, ultimately generating code that conforms to NuSMV syntax specifications. Secondly, each step is carried out in a strict linear flow, ensuring the systematization and orderliness of the conversion process. The process uses a pattern mapping table, explicitly mapping the original elements of the Stateflow model to the target NuSMV syntax, clarifying how each model element is converted to its corresponding formal expression. Finally, the entire process maintains consistent terminology, ensuring accurate correspondence between Stateflow and NuSMV domain terminology, thus avoiding ambiguities in the conversion process and ensuring semantic rigor and consistency.

3.5. Analysis of the Correctness of Model Transformation

It is crucial to ensure the correctness of model transformation in the development and validation process based on model transformation. Research on model transformation correctness can be divided into two levels: syntax and semantics. In general, when the model transformation is grammatically and semantically correct, it can be proven that the transformation is correct. We analyze the correctness of model transformation from the following four aspects.

1.: Grammar correctness

As an essential requirement for model transformation, the syntax correctness we need is that the transformed target model conforms to the target syntax rules. In the Stateflow SMV model conversion, a text model (i.e., a file with the suffix “.smv”) was generated based on the SMV text syntax template. This file can be opened in the validation tool NuSMV to obtain a formal model without errors, indicating that the converted model conforms to the SMV syntax rules.

2.: Grammatical completeness

The completeness we need is that the transformation rules completely cover the source model elements.

3.: Grammatical terminability

The terminability we need is that the source model must obtain a definite target model after completing a finite-step transformation. In Section 4.1 and Section 4.2, in Algorithms 1 and 2, the parsing of the source Stateflow model and the generation of the target model are completed within a finite number of steps, and the elements of the source and target models are 1:1 mapped. Therefore, the transformed target model is deterministic and unique.

4.: Semantic consistency

Semantic consistency is the most important criterion for model transformation, and we require that the pre-transformation and post-transformation models exhibit the same behavior when receiving the same input. When the two systems are mutually simulated equivalence, they can simulate each other’s actions. By simulating equivalence, we can define the equivalence relationship between two transfer systems; that is, when they simulate equivalence, they can simulate each other’s actions. For the Stateflow state machine before the transition and the time automaton SMV after the transition, according to the mapping rule of states in Section 3.3, each state

s f_s

in the Stateflow and the state

n m_s

of the SMV model obtained from the transition satisfy a mutual simulation relationship. i.e.,

(s f_s, n m_s) \in R

According to the mapping rules of variables and transfer, we ensure that the constraints and behavior of transfer before and after model transformation are the same. Thus, under the same input, after the same action

α

, the migration target state

n m_s

n m_s

is mapped from the migration target state

s f_s^{'}

s f_s

. Therefore,

s f_{s}^{'}

and

n m_{s}^{'}

also satisfy a mutual simulation relationship. According to the mapping rules, each model element of the Stateflow state machine and the SMV automaton is mapped individually.

Therefore, based on the definition of mutual simulation equivalence, we assume that the source Stateflow state machine and the target SMV time automaton satisfy the mutual simulation relationship, maintain behavioral equivalence, and maintain semantic consistency before and after model transformation.

4. Experiments and Tools

We use the process of a track section routing algorithm for a train interlocking system as a case study to demonstrate the application of our proposed method in the field of system modeling and validation. We enlarged one of the orbital node modules to achieve model conversion. Due to space limitations, we provide a portion of the code to demonstrate.

4.1. Case of Railway Section Route Algorithm

The routing algorithm for train tracks completes the search process by judging the coordinate properties of track nodes. During the search process, the interlocking system determines and searches for the next node internally based on the obtained node information. The system continuously loops to judge the nodes on each search path until the route is found or the end of the search is reached. After the end node of the route is selected, the interlocking system enters the following route search process (see Figure 8):

The search direction of the route is determiend based on the conditions in the judgeDirection operation;
Obtain the information of the starting node from the getNode operation and set it as the processing node Pp;
Determine whether the processing node Pp is a turnout section and whether it is an opposing turnout (switchDirection = searchDirection);
Determine whether there is a guide sign and determine the value of the next pointer nextP based on the vertical coordinates of the current node and the terminal node;
Determine whether this node is a terminal node or the end of the route search. If not, reset the node Pp being processed by the interlocking system to nextP.
Continue the search cycle for the next node until the end of the search when the terminal node is found, and record the nodes found. If the terminal node is not found when reaching the end of the search, an error message is returned.

The experimental data we designed were collected on a computer using an Intel (R) core (TM) i5-10210u [email protected] obtained on a computer with 2.10 GHz, 8 GB of memory, and a Windows 10 operating system. The conversion algorithm was implemented in Python and C languages. The pending information of the state diagram in this model can be divided into the following groups:

Lexical structure. Single word and sentence specifications for basic construction elements in model statements, including various variable elements;
Expression definition. Expressions specify symbolic, Boolean, and numerical expressions in model statements;
Instruction set definition. The instruction set specifies syntax conversion rules that describe specific conversion operations.

By processing this information, we use an analysis algorithm that conforms to the syntax rules of Stateflow to implement the transformation process and check the correctness of the transformed model according to the NuSMV protocol. All elements are drawn in MATLAB 2020b/SIMULINK tools, including state sets, transition events, and transition conditions. Afterward, we flatten the hierarchical relationships between composite states into single-layer states, extracting the sequential relationships between states and transitions into logical sets.

The names of all flattened state set elements are as follows:

VAR status: Idle, reverse Search, forwardSearch, reverseSearch_searchDirection, forwardSearch_searchDirection, turnoutType, judeSign, noteTurnoutNode, coordinated Difference, chosepfz, nextP_CheckPpfz, chosepfw, nextP_CheckPpfw, judeTerminal, routeFound, routeNotFound, judeEnd, nextNode;

Through the correspondence between the numerical ranges of the state model and the validation model, we have determined the limits and initial allocation of the transformed environmental variables. Due to the influence of MATLAB 2020b syntax, the basic types of state models used in the experiment include integer type, real number type, character data, logical value type, array data, etc. The integer types include multi-bit signed word and unsigned word integers. NuSMV supports Boolean, enumeration, signed, unsigned, array, and collection types.

The initialization of state and environment variables starts from the main module of the validation model. The pattern of state set transition determines the definition of state variables, and all reachable patterns must be enumerated at the beginning to complete the next transition process. The ASSIGN statement describes all initial states and transitions between states of the system. Each target state set SA, the migration target exits, and its corresponding transition in the migration set T and logical set L. We use init (var) to represent the initial assignment of the state variable var, use next (var) to represent the value of var in the next state, and use case ESAC to describe the substate syntax of variables, thereby transforming the example into a complete model (see Figure 9).

When instantiating a switch, we must provide its determined attribute values, such as switch number and type, in the UML model. Due to the unknown route information in the initial state, it is impossible to determine whether it is in the correct position in the turnout model. Therefore, we set the initial value of the correct position to 0, and the same applies to other attributes. The assigned code is shown in the figure. The correlation between various states in the state diagram is mainly used to reflect the hierarchical structure of the system and does not involve interlocking operations. When converting into a formal model, it should be omitted. It should be noted that the properties in both the parent and child states of the generalized relationship should be converted into the NuSMV submodule during the transformation.

4.2. Result Test

When we run this model in NuSMV, we can determine whether the model has achieved the expected effect by the jump state after inputting data. The two tables, Table 3 and Table 4, present the outputs of the model under two different input data sets, showcasing the different results for when a route is found and when a route is not found in the context of a train track routing system.

When the input Pb and other data can satisfy the path search requirements and obtain a complete path, the final output phase of the verification process can finally reach the route Found, as shown in Table 3. This table outlines the sequence of status updates after inputting a specific data set for the train routing algorithm. The initial inputs, represented as sets of points Pb and Pt, trigger the algorithm, and the system begins its search. The table tracks the state changes at each step of the process. The status evolves through different states, starting from “Idle” and transitioning through various phases such as “reverseSearch”, “switchType”, “coordinateDifference”, “judgeSign”, and “choosefw” as the model works through the nodes. Ultimately, after 33 steps, the status reaches “routeFound”, indicating the successful completion of the routing process, where the algorithm has found a valid path from the start point to the destination. In contrast, Table 4 follows a similar process but for a different input data set that does not lead to a valid route. Similar to Table 3, the system transitions through states like “reverseSearch”, “switchType”, “coordinateDifference”, and “choosefw”. However, unlike Table 3, this process continues for 41 steps without reaching a valid conclusion. Instead of ending with “routeFound”, it culminates in the “routeNotFound” status, indicating that the system was unable to find a route between the input points. This suggests either an issue with the node configuration or the lack of a valid path under the given conditions.

In order to test the state transition process and effectiveness of train switch equipment control stations more intuitively, we extracted the switch status module from the routing algorithm as an example of protocol detection, as shown in Figure 10. The model describes the state transitions of a switch in a train track system, which can be in either a “locked” or “unlocked” state. When in the “locked state”, the switch cannot be operated or change direction, which occurs when “section_status = 1” and “route_status = 1”. In contrast, the “unlocked state” allows the switch to operate and change direction, further dividing into two substates: “normal” and “reverse”. The transition between these substates depends on specific conditions. If “unlock = 1” and “out_normal = 1”, the switch moves to the “normal” state, while if “unlock = 1” and “out_reverse = 1”, it moves to the “reverse” state. The initial state is marked by a black dot, and transitions occur based on predefined conditions ensuring safe and controlled switching operations.

After the transition, all elements in the state diagram correspond to the corresponding language of SMV syntax (see Figure 11).

To verify the effectiveness of the transformation, we need to verify the reliability of the formal system model. Therefore, we collected some general normative semantics of switch-locking actions to form validation statements for model attributes.

Attribute 1 ensures that a train track switch cannot be unlocked if the section it belongs to is occupied by a train, thus maintaining railway safety. The formal verification formula is used for this property as follows, which checks that it is never possible for the section to be unoccupied (section_status = 0) and the route not to be set (route_status = 0) at the same time while the switch is being unlocked. In other words, the switch remains locked whenever the section is occupied by a train. Verification results confirm that this property holds true for various switches, meaning the system correctly prevents the switch from unlocking when a train occupies the section, ensuring safe track operations and preventing unintended route changes that could lead to accidents.

Attribute 1 . S P E C! E F (s e c t i o n_{s} t a t u s = 0 & r o u t e_{s} t a t u s = 0)

Attribute 2 ensures that when a switch is in the locked state, it cannot perform any operation to change its position, either to the normal or reverse state. This property is vital for system safety, as it prevents the switch from unintentionally changing direction or position while locked, which could lead to track conflicts or unsafe operations. The formal verification formula checks that when the switch is locked (unlock = 0), it cannot transition to either the normal (out_normal = 1) or reverse (out_reverse = 1) state. The results of the verification confirm that this property holds for all tested switches, ensuring that locked switches remain in their current position and do not undergo any directional changes, thus maintaining the integrity and safety of the track system.

Attribute 2 . S P E C! E F (u n l o c k = 0 & o u t n o r m a l = 1) & E X (o u t r e v e r s e = 1)), S P E C! E F (u n l o c k = 0 & o u t r e v e r s e = 1) & E X (o u t n o r m a l = 1))

After enumerating all attributes through CTL expressions, import them into the validation tool to officially test the above transformation model. Through attribute 1, we have checked that the train cannot be unlocked after entering the section to be unlocked. The results prove that the validation in the table is correct. For property 2, we have verified that locking actions cannot be performed when the switch is in a locked state. The verification results are shown in the Table 5 and Table 6.

Table 5 presents the results of the formal verification for Attribute 1, which ensures that a train track switch cannot be unlocked if the section it belongs to is occupied by a train. The verification is based on a CTL expression, which checks that the switch cannot be unlocked when the track section is unoccupied (section_status = 0) and the route is not set (route_status = 0). The verification is performed for multiple switches identified by their unique switch_ID. The table shows that for all switches tested (switch_ID = 1, 2, 5, 21), the formula holds true, confirming that these switches will remain locked if the section is occupied by a train. This result verifies that the system correctly prevents the switch from unlocking when the section is occupied, thereby ensuring safety by avoiding accidental operations under unsafe conditions.

Table 6 presents the results of the formal verification for Attribute 2, which ensures that when a switch is in the locked state, it cannot perform any operation to change its position, either to the normal or reverse state. The verification is based on two formulas that assert if the switch is locked (unlock = 0), it should not transition to either the normal state (out_normal = 1) or the reverse state (out_reverse = 1). The verification was conducted for several switches identified by their switch_ID. The results confirm that for all tested switches (switch_ID = 5, 3, 15, 21), the system correctly prevents the switch from changing direction when locked, as the formulas hold true in all cases. This ensures that no directional transitions occur while the switch is locked, thereby maintaining track integrity and preventing accidental or unsafe operations. The verification results validate the correct functioning of the switch control system under the locked condition, confirming that the system prevents any unintended movements of the switch, which is essential for safe train operations.

Table 7 presents a counterexample for Property 2, highlighting a scenario where the system fails to prevent a locked switch from transitioning to the reverse state. This indicates a flaw in the model where the system attempts an illegal state transition, despite the switch being locked. The verification tool identified this issue through a counterexample trace, revealing the specific conditions under which the failure occurred. This finding is important for refining the model, as it highlights the need for corrections to ensure that the system adheres strictly to the intended behavior where locked switches cannot transition between normal and reverse states.

The verification process for both properties demonstrates that the model behaves as expected in the majority of scenarios, successfully ensuring safety by preventing switches from being unlocked when sections are occupied and from transitioning between states when locked. However, the counterexample presented in Table 7 reveals a critical issue where the system fails to prevent a transition for a locked switch. This issue needs to be addressed to ensure full compliance with the safety rules. The verification results show that the system largely meets its safety goals, but the counterexample provides valuable insight into areas for further refinement in the model.

4.3. Tools and Verification

Figure 11, Figure 12 and Figure 13 demonstrated the dynamic flow of information in the interlocking system during the route search process. The search begins with the input of the start node Pb and end node Pt coordinate sets, from which the system determines the initial search direction based on coordinate differences (such as comparing Pb.X with Pt.X). The interlocking system then acquires the start node information, sets it as the current processing node Pp, and enters a loop of judgment. Within the loop, the system first checks if Pp is a switch section and determines the validity of the path branch by comparing the switch direction with the search direction (switchDirection == searchDirection). If the switch is in the unlocked state, the system calculates a guiding flag based on the vertical coordinate relationship between the current node and the destination (e.g., the difference between Pb.Y and Pt.Y), and dynamically updates the pointer value of the next target node, nextP. If Pp is not the terminal node, the system sets nextP as the new processing node and repeats the judgment process, gradually approaching the destination.

During the search, the interlocking system continuously monitors node attributes and state conditions (such as section occupation status and switch position correctness) to ensure the path’s feasibility and safety. If the system encounters an unmatched node or triggers an end condition (such as exhausting the search attempts), it will return an error. Otherwise, when the terminal node coordinates are successfully matched, the search concludes and is marked as “routeFound”. The red information flow in Figure 12 clearly shows the complete link from the initial state to the successful route determination. The state transition sequence (as seen in Table 3) further validates the model’s core logic of dynamically coordinating coordinate judgments, switch state changes, and node iteration updates, ultimately completing the route search efficiently.

Whenever a node is determined to be a non-terminal node (Pb.terminal == 0), the system resets “Pp” to “nextP” and proceeds to the next round of the search. This process is repeated, involving steps such as coordinate difference calculation, direction verification, and node type determination. However, due to the input data’s coordinate distribution failing to form a valid path (e.g., overlapping coordinate ranges or path interruptions), the system is unable to match the terminal node after multiple attempts. Ultimately, after numerous state transitions (as shown in Table 4), all possible paths are explored without meeting the termination conditions, and the system returns a “routeNotFound” error, indicating that the route search has failed, as shown in Figure 13. This entire process reflects the interlocking system’s characteristic of dynamically adjusting the search path through progressive judgments based on coordinate attributes and direction logic. The core issue lies in the adaptability of the coordinate data and the strictness of the direction rules. When the input data does not meet the continuity of the path, the system can fully execute the search logic but is unable to reach the expected destination.

In addition to finding pathways, another important role of verification is to help us locate some external fault locations. When we perform protocol validation on the switch status module model Figure 10, the tool provides path feedback based on the output report.

The red text in Figure 14 highlights the fault location where the system encountered an issue. This failure occurs when the turnout cannot transition as expected due to incorrect input conditions or mismatched data. The red arrows and highlighted conditions indicate that although the transition conditions for the unlocking process (from locked to unlocked) were met, the system was unable to complete the transition successfully due to a discrepancy, failing to align the turnout in the correct position or proceed with the route setup. This validation provides insights into where the model is not performing as expected, specifically identifying that the system was unable to correctly update the turnout’s position based on the given input data, which ultimately caused the route to fail. We can correct erroneous path errors to achieve the purpose of model validation.

5. Conclusions and Prospect

This study proposes a UML state diagram semantic abstraction and transformation method for symbol verification. In order to more accurately simulate the dynamic behavior of state objects in their lifecycle, we have completed model abstraction at the meta-model level, abstracting state graphs into semantic models, establishing semantic mapping rules for states and transition processes, and proving their effectiveness through theorems. For specific railway switch routing examples, we use the modeling tool MATLAB Simulink’s Stateflow state diagram tool to model, convert it into the corresponding validation model, and then use NuSMV to simulate and validate the content in the software process. The output results of the case indicate that the proposed method is highly effective for modeling, simulation, transformation, and validation of natural software processes.

The development of software systems is a process of gradually refining software models, which requires introducing more details from the overall model with higher levels of abstraction until sufficient information is obtained to describe the specific model of the system. During this period, the structure and semantics between models should be consistent. Although industry researchers have reached a consensus on the static semantics of UML (UML accurately defines the relevant “syntax” section in its official manual but only considers the “static semantics” section in compilation theory, which includes English prose and is not unrelated to the previous text, thus lacking accuracy and completeness), However, semantic refinement and transformation validation of UML dynamic behavior diagrams (including interaction diagrams, activity diagrams, and state diagrams) remains a challenging and essential task. In addition, a large amount of research is being conducted on how to use appropriate expression methods to achieve attribute transformation in dynamic models and prove the correctness of all these theorems.

In 2016, Celebi expressed the content of the interlocking table in the form of an abstract state machine and transformed it into a NuSMV state transition model, achieving formal verification of the interlocking system [10]. In [14], a series of structured modeling semantics for the UML state diagram of the validation tool Coq were described, and the correctness of its semantics was demonstrated through the theorem proving tool Cqi’s normalization and label transfer system. The state of the state machine is mapped to the term algebra on the transition system LTS marked in [25], and the semantics of the UML state machine are summarized through structural operation semantic SOS rules. Reference [26] introduced the abstract state automaton theory and method of calculus, proposed the semantic specification of dynamic graphs (including activity graphs, state graphs, and sequence graphs), and validated the elevator instance model based on this specification. In [27], the syntax structure of the state machine was described. Then, the operational semantics of the state machine were formalized using the RAISE description language RSL, which explains the generation of triggering events, establishment of transitions, completion of operations, conflicts, and priority selection of the state machine. References [28,29,30,31,32,33,34,35,36,37] presents the meta-model integration of UML in different views, including interaction diagrams, sequence diagrams, and state machine diagrams. By extending Buchi automata, Kripke computational tree logic, and abstract essence, the formal transformation from state models to validation models is completed. References [38,39,40] focus on introducing the project example. After completing the requirements modeling steps, a corresponding fault extension model was designed based on the system, and fault analysis and system safety evaluation were conducted on the relevant real-time interlocking control system.

Our work plays a crucial role in ensuring the real-time functionality of the train track routing system and its dynamic behavior during operation. Real-time systems, such as train switch systems, are highly sensitive to time constraints, and accurate state transitions and timely responses are crucial for safe and efficient operation. In the context of our model, the route search process emphasizes the real-time requirements of the system. When the system searches for effective paths by tracking nodes, it continuously checks and updates node conditions based on the current status and search progress. When the train interacts with the switch and track section, it is crucial that the system not only performs the correct conversion but also performs the conversion within the specified time limit to ensure the continuity of the search and the safety of the train operation. Our validation method can simulate these state transitions, especially for switch models. When the switch is in a locked state, it cannot change direction, ensuring that the system does not allow conflicting operations at critical moments. Once the switch is unlocked, the system dynamically determines whether to move the switch to the normal or reverse state, which must occur within a strict time window. This real-time verification ensures that every state change, such as moving from one track segment to another, occurs within a specified delay (e.g., “0.5 s later” in Figure 9), and that the system always adheres to the security protocol.

In addition, the MDA allows us to generate formal code from UML state machine diagrams, which can then be validated using tools such as NuSMV. This allows for automated real-time validation of the system, ensuring that conversions and responses occur within the required time frame, and ensuring that the system remains consistent with its expected behavior under various conditions. The ability to perform these checks in real time is crucial for preventing malfunctions and ensuring that the system can handle operations simultaneously, such as activating multiple switches or handling multiple trains simultaneously.

Compared with previous work, this article uses mathematical theory-based methods for model analysis, transformation, and validation, explaining substantive issues in formal transformation and establishing semantic associations between abstract models and validation entities. In the future, we will further evaluate the methods we propose on various software projects (including open-source projects) to explore the efficiency of universal model transformation methods.

Author Contributions

Conceptualization, R.W. and Y.D.; methodology, R.W.; software, R.W. and Y.D.; validation, R.W., Y.D. and M.L.; formal analysis, Y.D.; investigation, R.W.; resources, R.W.; data curation, R.W.; writing—original draft preparation, R.W.; writing—review and editing, Y.D. and M.L.; visualization, R.W.; supervision, Y.D.; project administration, Y.D. All authors have read and agreed to the published version of the manuscript.

Funding

This research was supported by the Fundamental Research Funds for the Central Universities (No. 2024JBZX018), the National Key Research and Development Program of China (No. 2022YFB3105105), and the Central Guidance for Local Scientific and Technological Development Fund (No. 246Z0705G).

Institutional Review Board Statement

Our study did not require further ethics committee approval as it did not involve animal or human clinical trials and was not unethical. According to the ethical principles outlined in the Declaration of Heart of Helsinki, all participants provided informed consent prior to participating in the study. Participants’ anonymity and confidentiality were guaranteed, and participation was entirely voluntary.

Data Availability Statement

The original contributions presented in this study are included in the article. Further inquiries can be directed to the corresponding author.

Conflicts of Interest

The authors declare no conflicts of interest. The funders had no role in the design of the study; in the collection, analyses, or interpretation of data; in the writing of the manuscript; or in the decision to publish the results.

Appendix A

Appendix A.1

Table A1. Matlab Antlr4 syntax rules used in engineering.

Type	Syntax Format	Explain
primary_expression	IDENTIFIER	Identifier,[a-zA-Z][a-zA-Z0-9]*
	CONSTANT	constant (numeric type)
	STRING_LITERAL	text string (string type)
	‘(’expression‘)’	‘(’Axpressions‘)’
	‘[’ ‘]’	‘(’axpressions‘)’ empty array
	‘[’array_list‘]’	array type (non empty) ‘[’array‘]’
postfix_expression	primary_expression	basic expression
	function_expression	functional expression
	array_expression	array expression
	postfix_expression TRANSPOSE	postfix expression (self) transpose identifier
	postfix_expression NCTRANSPOSE	suffix expression (itself) for a certain identifier
index_expression	‘:’	Single colon ‘:’
index_expression	expression	expression
index_expression_list	index_expression	index expression (single)
index_expression_list	index_expression_list ‘,’ index_expression	index expression (list itself) and index expression (single), comma separated
function_expression	FUNCTIONID ‘(’index_expression_list‘)’	special function identifier and index expression (list) as parameters
array_expression	IDENTIFIER ‘(’index_expression_list‘)’	identifier and index expression (list)
unary_expression	postfix_expression	postfix expression
unary_expression	unary_operator postfix_expression	unary operator suffix expression
unary_operator	‘+’	monocular (unary) operator, a single operand, takes a positive value
	‘−’	monocular (unary) operator, single operand, takes negative values
	‘~’	monocular (unary) operator, single operand, bitwise inversion
	additive_expression ‘+’ multiplicative_expression	addition expression (self) ‘+’ multiplication expression
	additive_expression ‘−’ multiplicative_expression	addition expression (self) ‘−’ multiplication expression
math_expression	postfix_expression	postfix Expression
	math_expression ‘*’ postfix_expression	mathematical expression (itself) ‘*’ suffix expression
	math_expression ‘/’ postfix_expression	mathematical expression (self) ‘/’ suffix expression
	math_expression ‘\\’ postfix_expression	Mathematical expression (itself) ‘\\’ suffix expression
	math_expression ‘^’ postfix_expression	mathematical expression (itself) ‘^’ suffix expression
	math_expression ARRAYMUL postfix_expression	mathematical expression (itself) ‘. *’ postfix Expression
	math_expression ARRAYDIV postfix_expression	mathematical expression (itself) ‘. \\’ postfix Expression
	math_expression ARRAYRDIV postfix_expression	mathematical expression (itself) ‘./’ postfix Expression
	math_expression ARRAYPOW postfix_expression	mathematical expression (itself) ‘.^’ postfix expression
	math_expression ‘+’ postfix_expression	mathematical expression (itself) ‘+’ suffix expression
	math_expression ‘−’ postfix_expression	mathematical expression (self) ‘−’ suffix expression
	equality_expression EQ_OP relational_expression	equation expression (itself) ‘==’ relationship expression
	equality_expression NE_OP relational_expression	Equation expression (self) ‘~=’ relationship expression
relational_expression	math_expression	mathematical expression
	relational_expression ‘<’ math_expression	relation expression (itself) ‘<’ mathematical expression
	relational_expression ‘>’ math_expression	relationship expression (self) ‘>’ mathematical expression
	relational_expression LE_OP math_expression	relation expression (self) ‘<=’ mathematical expression
	relational_expression GE_OP math_expression	relation expression (self) ‘>=’ mathematical expression
	relational_expression EQ_OP math_expression	relation expression (itself) ‘==’ mathematical expression
	relational_expression NE_OP math_expression	relation expression (self) ‘ =’ mathematical expression
logic_expression	relational_expression	relational expression
	logic_expression ‘&&’ relational_expression	logical expression (itself) ‘&&’ relational expression
	logic_expression ‘\|\|’ relational_expression	logical expression (itself) ‘\|\|’ relational expression
expression	or_expression	‘Or’ type expression
expression	expression ‘:’ or_expression	expression (itself) ‘:’ ‘Or’ type expression
assign_expression	postfix_expression ‘=’ expression	suffix expression ‘=’ expression
eostmt	‘,’	separate with commas ‘,’
	‘;’	semicolon ‘;’ separate
	CR	Line break character ‘∖r’ or ‘∖n’

Appendix A.2

Table A2. Matlab Antlr4 grammar rules used in engineering.

Type	Grammar Format	Explain
statement	global_statement	global statement
	clear_statement	clear variable statements
	assign_statement	assignment type statement
	expression_statement	expression statement
statement_list	statement	program statement (single)
statement_list	statement_list statement	program statement segment (itself)+program statement (individual)
identifier_list	IDENTIFIER	identifier (single)
identifier_list	identifier_list IDENTIFIER	identification list (self) and identifier (single)
clear_statement	CLEAR identifier_list eostmt	clear variable identifier ‘clear’ and identification list and delimiter
expression_statement	eostmt	delimiter
expression_statement	expression eostmt	expression and delimiter
assign_statement	assignment_expression eostmt	assignment type expression and delimiter
array_element	expression	expression (single)
array_element	expression_statement	expression statement
array_list	array_element	array element (single)
array_list	array_list array_element	array (itself) and array element (single)
translation_unit	statement_list	program statement segment
translation_unit	FUNCTION function_declare eostmt statement_list	runction identifier ‘function’ and function declaration (overall) and delimiter and program statement segment
func_ident_list	IDENTIFIER	identifier (single)
func_ident_list	func_ident_list ‘,’ IDENTIFIER	unary operator suffix expression
func_return_list	IDENTIFIER	identifier (single)
func_return_list	[’func_ident_list‘]’	[function definition List (parameters)‘]’
function_declare_lhs	IDENTIFIER	identifier (single)
	IDENTIFIER ‘(’ ‘)’	identifier (single) and ‘()’
	IDENTIFIER ‘(’func_ident_list‘)’	identifier (single) ‘(’function definition list‘)’
function_declare	function_declare_lhs	function declaration (function name)
function_declare	func_return_list ‘=’ function_declare_lhs	function return value list ‘=’ function declaration (function name)

References

Latella, D.; Majzik, I.; Massink, M. Towards a Formal Operational Semantics of UML Statechart Diagrams. In International Conference on Formal Methods for Open Object-Based Distributed Systems; Springer: Boston, MA, USA, 1999. [Google Scholar]
Wang, J.; Tang, Y.; Yu, H. Method of UML Statechart Checking Based on Explicit Model Checking. In Proceedings of the 2020 International Conference on Applications and Techniques in Cyber Intelligence, Fuyang, China, 20–22 June 2020. [Google Scholar]
Caltais, G.; Leitner-Fischer, F.; Leue, S. SysML to NuSMV Model Transformation via Object-Orientation. Transp. Probl. Int. Sci. J. 2017, 10107, 31–45. [Google Scholar]
Kim, Y.; Gomez, M.; Goppert, J. Model Checking of a Training System Using NuSMV for Humanoid Robot Soccer. In Robot Intelligence Technology and Applications 3. Advances in Intelligent Systems and Computing; Springer: Berlin/Heidelberg, Germany, 2015; pp. 531–540. [Google Scholar]
Havelund, K.; Penix, J.; Visser, W. SPIN Model Checking and Software Verification. In Proceedings of the 7th International SPIN Workshop, Stanford, CA, USA, 30 August–1 September 2000. [Google Scholar]
Florentin, I.; Raluca, L.; Cristina, T. Formal Verification of P Systems Using SPIN. Int. J. Found. Comput. Sci. 2011, 22, 133–142. [Google Scholar]
Latella, D.; Majzik, I.; Massink, M. Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker. Form. Asp. Comput. 1999, 11, 637–664. [Google Scholar] [CrossRef]
Farid, A.; AnneLise, C.; Thomas, L. Formal verification of a telerehabilitation system through an abstraction and refinement approach using Uppaal. IET Softw. 2023, 17, 582–599. [Google Scholar]
Sakata, K.; Fujita, S.; Sawada, K.; Iwasawa, H.; Endoh, H.; Matsumoto, N. Model verification of fallback control system under cyberattacks via UPPAAL. Adv. Robot. 2023, 37, 156–168. [Google Scholar] [CrossRef]
Celebi, B.T.; Kaymakci, O. Verifying the accuracy of interlocking tables for railway signalling systems using abstract state machines. J. Mod. Transp. 2016, 24, 277–283. [Google Scholar] [CrossRef]
Ahmad, M.; Yazdi, M. Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Transp. Probl. Int. Sci. J. 2009, 4, 103–110. [Google Scholar]
He, T.; Li, H.; Qin, G. Model Checking Analysis of Observational Transition System with SMV. In Proceedings of the Information Computing and Applications: Second International Conference, ICICA 2011, Qinhuangdao, China, 28–31 October 2011; pp. 537–544. [Google Scholar]
Börger, E.; Cavarra, A.; Riccobene, E. Modeling the Dynamics of UML State Machines. In International Workshop on Abstract State Machines, Theory and Applications; Springer: Berlin/Heidelberg, Germany, 2000; pp. 223–241. [Google Scholar]
Sheng, F.; Dou, L.; Yang, Z.Y. Mechanized semantics and refinement of UML-Statecharts. Front. Inf. Technol. Electron. Eng. 2017, 18, 108–119. [Google Scholar] [CrossRef]
Chu, H.; Li, Q.; Hu, S.; Chen, P. An Approach for Reversely Generating Hierarchical UML Statechart Diagrams; Springer: Berlin/Heidelberg, Germany, 2006. [Google Scholar]
Cimatti, A.; Clarke, E.; Giunchiglia, E. NuSMV: A New Symbolic Model Verifier. In Proceedings of the Computer Aided Verification: 11th International Conference, CAV’99, Trento, Italy, 6–10 July 1999; pp. 495–499. [Google Scholar]
Cimatti, A.; Clarke, E.; Giunchiglia, E. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In Proceedings of the Computer Aided Verification: 14th International Conference, CAV 2002, Copenhagen, Denmark, 27–31 July 2002. [Google Scholar]
Biere, A.; Cimatti, A.; Clarke, E.; Giunchiglia, E. Symbolic Model Checking Without BDDs. In Proceedings of the TACAS’99, Amsterdam, The Netherlands, 22–28 March 1999; pp. 495–499. [Google Scholar] [CrossRef]
Hu, J.; Wu, X.; Dong, Y.; Zhang, F. Implementing the Compiler of AADL Behavior Annex Using ANTLR. In Proceedings of the 2011 IEEE 2nd International Conference on Software Engineering and Service Science, Beijing, China, 15–17 July 2011; pp. 221–225. [Google Scholar]
Jean, B.; Terence, P. ANTLRWorks: An ANTLR grammar development environment. Softw. Pract. Exp. 2008, 38, 1305–1332. [Google Scholar]
Rabah, M.; Allaoua, C. Compiling, verifying and simulating dynamic software architectures using ANTLR and coloured-ADL. Int. J. Commun. Networks Distrib. Syst. 2017, 19, 406–433. [Google Scholar]
Trancony, W.; Lepper, M.; Wieland, J. Automatic Construction of XML-Based Tools Seen as Meta-Programming. Autom. Softw. Eng. 2003, 10, 23–38. [Google Scholar] [CrossRef]
Feng, F.X.; Sen, G. XMI-based transformation from UML model to XML schema. J. Anhui Univ. Technol. Sci. 2007, 44–46, 22. [Google Scholar]
Hu, J.; Chen, S.; Chen, D. An ANTLR-based Flattening Framework for AltaRica 3.0 Model. Int. J. Perform. Eng. 2019, 15, 2462. [Google Scholar]
Jiang, H.; Lin, D.; Xie, X.R. The Formal Semantics of UML State Machine. J. Softw. 2002, 13, 7. [Google Scholar]
McUmber, W.; Cheng, B. A general framework for formalizing UML with formal languages. In Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, Toronto, ON, Canada, 12–19 May 2001; pp. 433–442. [Google Scholar] [CrossRef]
Chen, W. The Formal Semantic Study of UML State Machine. Ph.D. Thesis, Southwest University, Chongqing, China, 2004. [Google Scholar]
Shan, L.J.; Zhu, H. A Formal Descriptive Semantics of UML. Comput. Eng. Sci. 2010, 32, 96–103. [Google Scholar]
Guo, Y.Y.; Zhang, N.; Tong, X.R. Survay on Formal Semantics of UML Sequence Diagram. Comput. Sci. 2017, 44, 15. [Google Scholar]
Fan, Y.H.; Li, Y.M.; Pan, H.Y. Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke structure. Acta Electron. Sin. 2018, 46, 8. [Google Scholar]
Yi, J.; Zhang, W.H. Effecient Transformation Transition Based Generalized Buchi Automatato Buchi Automata. J. Softw. 2006, 17, 720. [Google Scholar] [CrossRef]
Guo, Y.Y.; Liu, J.L. Formalization for Model Element of UML Statechart in RSL. Comput. Sci. 2013, 40, 177–183+205. [Google Scholar]
Xu, M.; Kai, J.Y. A Tool to Convert XMI to SMV in Python. J. Fuzhou Univ. Nat. Sci. Ed. 2014, 42, 50–54. [Google Scholar]
Liu, Z. Formal Modeling and Verification of Interlocking Software based on UML-NuSMV. Master’s Thesis, Lanzhou Jiaotong University, Qinghai, China, 2018. [Google Scholar]
Guo, L.; Miao, H.K.; Wang, X.; Chen, S.B. Transformation from UML Model to FSM Model. Comput. Sci. 2009, 36, 5. [Google Scholar]
Chama, W. Model Checking and Code Generation for UML Diagrams Using Graph Transformation. Int. J. Softw. Eng. Appl. 2012, 3, 39–55. [Google Scholar] [CrossRef]
Liu, C.; Jiang, Y.P.; Ma, C.Y.; Zhang, T. Formal verification technology for AADL models based on NuSMV. Acta Aeronaut. Astronaut. Sin. 2022, 43, 325196. [Google Scholar]
Zhang, W.J.; Hu, J.; Li, W.Q.; Chen, S.; Shi, M.H.; Tang, H.Y. Case Study of Formal Modeling Analysis for Safety-Critical System Requirements. J. Front. Comput. Sci. Technol. 2019, 13, 12. [Google Scholar]
Wang, M.M.; Luo, Y. Test Case Generation Method Based on Extended Finite State Machine. Electron. Des. Eng. 2020, 28, 5. [Google Scholar]
Luan, J.W.; Wu, C. Research on Strategy of Test Case Generation Based on UML Statechart. Comput. Digit. Eng. 2020, 48, 409. [Google Scholar]

Figure 1. The overall process of model-driven architecture.

Figure 2. Framework diagram of model detection knowledge logic.

Figure 3. Schematic diagram of real-time system formal verification.

Figure 4. Decomposing a language into a syntax tree (AST).

Figure 5. Process of model transform from Stateflow to SMV.

Figure 6. Performing lexical and grammatical analysis on information through ANTLR.

Figure 7. Converting based on a complete NuSMV specification template.

Figure 8. State diagram of railway section route algorithm.

Figure 9. Example of partial element transformation in the model.

Figure 10. State diagram of railway turnout state transition.

Figure 11. State diagram of railway turnout state transition.

Figure 12. State Diagram of Railway Turnout State Transition. The red information flow shows thecomplete link from the initial state to the successful route determination.

Figure 13. State diagram of railway turnout state transition. The red information flow shows thecomplete link from the initial state to the routeNotFound determination.

Figure 14. State diagram of railway turnout state transition.

Table 1. Formal tools exhibit differentiated features in real-time system validation.

Tool	Main Advantage	Application Case	Limitation
NuSMV	Symbolic model checking supports CTL/LTL	Alstom train control system deadlock verification	Weak real-time attribute modeling capability
UPPAAL	Time automata and clock constraints	Siemens rail transit signal timing compliance verification	Explosion problem of complex system states
SPIN	Distributed process interaction verification	NASA Mars rover mission scheduling verification	Manually writing Promela code is inefficient

Table 2. Mapping rules for Simulink/Stateflow to SMV.

No.	Element in Stateflow	Element in SMV
1	logical	Boolean
2	integers	integer
3	Single/Double	signed/unsigned
4	state	state
5	$i n i t i a l_s t a t e$	$s t a t e_{0}$
6	$f i n a l_s t a t e$	$s t a t e_{f}$
7	transition	transition
8	event	Condition
9	guard	Constraint
10	action	Action

Table 3. Run of model to be validated: routeFound.

→ insert:
Pb set: {(55,64), (6,76), (12,63), (76,97), (92,39), (99,82), (24,67), (30,45), (91,52), (52,47)};
Pt set: {(38,37), (87,55), (91,93), (58,23), (34,16), (61,58), (12,92), (19,71), (95,18), (23,66)};
→ running:
0 status = Idle	17 status = judgeEnd
1 status = reverseSearch	18 status = nextNode
2 status = reverseSearch_searchDirection	19 status = nextNode
3 status = switchType	20 status = switchType
4 status = judgeSign	21 status = judgeSign
5 status = coordinateDifference	22 status = coordinateDifference
6 status = chosepfw	23 status = chosepfw
7 status = chosepfw	24 status = judgeTerminal
8 status = judgeTerminal	25 status = judgeEnd
9 status = judgeEnd	26 status = nextNode
10 status = nextNode	27 status = nextNode
11 status = nextNode	28 status = switchType
12 status = switchType	29 status = judgeSign
13 status = judgeSign	30 status = coordinateDifference
14 status = coordinateDifference	31 status = chosepfw
15 status = chosepfw	32 status = judgeTerminal
16 status = judgeTerminal	33 status = routeFound

Table 4. Run of model to be validated: routeNotFound.

→ insert:
Pb set: {(78,86), (52,4), (74,92), (68,61), (88,75), (75,95), (35,37), (31,70), (73,69), (77,65)};
Pt set: {(48,41), (87,17), (93,9), (20,55), (72,1), (57,26), (99,5), (3,36), (17,70), (80,54)};
→ running:
0 status = Idle	21 status = judgeSign
1 status = reverseSearch	22 status = coordinateDifference
2 status = reverseSearch_searchDirection	23 status = chosepfw
3 status = switchType	24 status = judgeTerminal
4 status = judgeSign	25 status = judgeEnd
5 status = coordinateDifference	26 status = nextNode
6 status = chosepfw	27 status = nextNode
7 status = chosepfw	28 status = switchType
8 status = judgeTerminal	29 status = judgeSign
9 status = judgeEnd	30 status = coordinateDifference
10 status = nextNode	31 status = chosepfw
11 status = nextNode	32 status = judgeTerminal
12 status = switchType	33 status = judgeEnd
13 status = judgeSign	34 status = nextNode
14 status = coordinateDifference	35 status = switchType
15 status = chosepfw	36 status = judgeSign
16 status = judgeTerminal	37 status = coordinateDifference
17 status = judgeEnd	38 status = chosepfw
18 status = nextNode	39 status = judgeTerminal
19 status = nextNode	40 status = judgeEnd
20 status = switchType	41 status = routeNotFound

Table 5. Run of Specification Verification 1: true case.

Property 1.

→ insert: SPEC ! EF(section_status = 0 & route_status = 0)

→ running:

–specification ! EF(switch_ID=1 & section_status = 0 & route_status = 0) is true

–specification ! EF(switch_ID=2 & section_status = 0 & route_status = 0) is true

–specification ! EF(switch_ID=5 & section_status = 0 & route_status = 0) is true

–specification ! EF(switch_ID=21 & section_status = 0 & route_status = 0) is true

Table 6. Run of Specification Verification 2: true case.

Property 2.

→ insert:

SPEC ! EF((unlock = 0 & out_normal = 1)&EX(out_reverse = 1))

SPEC ! EF((unlock = 0 & out_reverse = 1)&EX(out_normal = 1))

→ running:

–specification ! EF((switch_ID = 5 & unlock = 0 & out_normal = 1)

& EX(switch_ID = 5 & out_reverse = 1)) is true –specification ! EF((switch_ID = 3

& unlock = 0 & out_normal = 1)

& EX(switch_ID = 3 & out_reverse = 1)) is true –specification ! EF((switch_ID = 15

& unlock = 0 & out_normal = 1)

& EX(switch_ID = 15 & out_reverse = 1)) is true –specification ! EF((switch_ID = 21

& unlock = 0 & out_normal = 1)

& EX(switch_ID = 21 & out_reverse = 1)) is true

Table 7. Run of Specification Verification 2: true case.

Property 2.

→ insert:

SPEC ! EF((unlock = 0 & out_normal = 1)&EX(out_reverse = 1))

SPEC ! EF((unlock = 0 & out_reverse = 1)&EX(out_normal = 1))

→ running:

–specification ! EF((unlock = 0 & out_normal = 1)& EX(out_reverse = 1)) is false

–as demonstrated by the following execution sequence

Trace Type: Couterexample

→ State:1.1 ←

SW5_state = 0

SW7_state = 0

SW5_unlock = 0

SW5_normal = 1

SW6_unlock = 1

SW6_LOCK = 0

SW6_normal = 1

→ State:1.2 ←

…

Disclaimer/Publisher’s Note: The statements, opinions and data contained in all publications are solely those of the individual author(s) and contributor(s) and not of MDPI and/or the editor(s). MDPI and/or the editor(s) disclaim responsibility for any injury to people or property resulting from any ideas, methods, instructions or products referred to in the content.

© 2025 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (https://creativecommons.org/licenses/by/4.0/).

Share and Cite

MDPI and ACS Style

Wu, R.; Du, Y.; Li, M. A Model Transformation Method Based on Simulink/Stateflow for Validation of UML Statechart Diagrams. Mathematics 2025, 13, 724. https://doi.org/10.3390/math13050724

AMA Style

Wu R, Du Y, Li M. A Model Transformation Method Based on Simulink/Stateflow for Validation of UML Statechart Diagrams. Mathematics. 2025; 13(5):724. https://doi.org/10.3390/math13050724

Chicago/Turabian Style

Wu, Runfang, Ye Du, and Meihong Li. 2025. "A Model Transformation Method Based on Simulink/Stateflow for Validation of UML Statechart Diagrams" Mathematics 13, no. 5: 724. https://doi.org/10.3390/math13050724

APA Style

Wu, R., Du, Y., & Li, M. (2025). A Model Transformation Method Based on Simulink/Stateflow for Validation of UML Statechart Diagrams. Mathematics, 13(5), 724. https://doi.org/10.3390/math13050724

Note that from the first issue of 2016, this journal uses article numbers instead of page numbers. See further details here.

Article Menu

A Model Transformation Method Based on Simulink/Stateflow for Validation of UML Statechart Diagrams

Abstract

1. Introduction

2. Basic Knowledge

2.1. UML State Machine Based on Simulink/Stateflow

2.2. SMV Model Based on Symbol Verification

2.3. Principles of Syntax Parsing Based on ANTLR

3. Model Transform: From Simulink/Stateflow to NuSMV

3.1. Information Extraction

3.2. State Refinement

3.3. Semantic Mapping

3.4. Grammar Conversion

3.5. Analysis of the Correctness of Model Transformation

4. Experiments and Tools

4.1. Case of Railway Section Route Algorithm

4.2. Result Test

4.3. Tools and Verification

5. Conclusions and Prospect

Author Contributions

Funding

Institutional Review Board Statement

Data Availability Statement

Conflicts of Interest

Appendix A

Appendix A.1

Appendix A.2

References

Share and Cite

Article Metrics

Article Access Statistics

Further Information

Guidelines

MDPI Initiatives

Follow MDPI