# Modeling and Analysis of Cyber-Physical Systems in the Hybrid π-Calculus Using Extended Sequence Diagrams

Xiong Xu, Jixiang Miao, Shuling Wang, Jean-Pierre Talpin

► To cite this version:

Xiong Xu, Jixiang Miao, Shuling Wang, Jean-Pierre Talpin. Modeling and Analysis of Cyber-Physical Systems in the Hybrid π-Calculus Using Extended Sequence Diagrams. ICFEM 2025 - 26th International Conference on Formal Engineering Methods, Nov 2025, Hang Zhou, China. pp.60-78, 10.1007/978-981-95-4213-0_4 . hal-05532526

HAL Id: hal-05532526

https://hal.science/hal-05532526v1

Submitted on 2 Mar 2026

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Modeling and Analysis of Cyber-Physical
Systems in the Hybrid π-Calculus Using
Extended Sequence Diagrams

Xiong Xu¹[0000-0003-4236-9992], Jixiang Miao¹,², Shuling Wang¹*[0000-0002-2798-2660], and Jean-Pierre Talpin³[0000-0002-0556-4265]

¹ National Key Laboratory of Space Integrated Information System, Institute of Software, Chinese Academy of Sciences, Beijing, China

² University of Chinese Academy of Sciences, Beijing, China

³ INRIA, Rennes, France

**Abstract.** Digital infrastructures, grids, and networks heavily rely on Cyber-Physical Systems (CPSs) endpoints in a context of mobile computing, referred to as mobile CPSs, including applications such as smart cities, intelligent transportation systems, and unmanned vehicles. Most of such systems are safety-critical, i.e., any error may result in catastrophic consequences. Mobile CPSs represent a novel computing paradigm, and their inherent complexity and interdisciplinary nature pose significant challenges to system design beyond the limits of state-of-the-art separation of concerns. Model-Based Design (MBD) is a key approach to mitigate the complexity of safety-critical systems. However, it lacks adequate modeling and analysis techniques to tame mobile CPSs. To address this gap, this paper proposes an extension of sequence diagrams, as found in SysML/UML, to facilitate an accurate, graphical representation of the deeply-coupled mobile, parallel, and hybrid behaviors (i.e., the entangled interplay of discrete and continuous behaviors). To ensure the correctness of the designed models, we propose a set of transformation rules that convert the (graphical and hence, by nature, informal) extended sequence diagram to a formal representation using the hybrid π-calculus, thereby enabling formal verification using, e.g., bisimulation-based model checking. Finally, we provide a case study where we employ extended sequence diagrams to model the scenario of the handover protocol of a train control system and formalize it into a hybrid π-calculus model using the proposed transformation rules.

**Keywords:** CPS · MBD · Sequence diagrams · Hybrid π-calculus · SysML/UML · Mobile computing and communication

# 1 Introduction

With the rapid development of 5G, 6G, real-time wireless, and integrated air-space-ground networks, an era of ubiquitous computing is emerging [7, 2, 6] fea-

<footnote>* Corresponding author (wangsl@ios.ac.cn).</footnote>
turing the integration of social, digital, and physical worlds. The fundamen-
tal characteristics of this paradigm include the interconnection of all entities,
software-defined everything, universal programmability, and natural interactions
among humans, machines, and physics. The dynamic environments, diverse re-
quirements, and complex physical scenarios introduced by mobile computing
necessitate that hardware resources, data resources, software platforms, and
applications possess flexible, software-defined capabilities, dynamic topologies,
adaptability, mobile interoperability, and natural interaction capabilities. Cyber-
Physical Systems (CPSs) in the context of mobile computing, referred to as mo-
bile CPSs, represent a novel computing paradigm whose significance has been
widely recognized. In particular, the design of safety-critical CPSs spans multi-
ple disciplines, including computer science, control theory, applied mathematics,
communication theory, and artificial intelligence. Their inherent complexity and
interdisciplinary nature pose great challenges to system design.

Model-Based Design (MBD) has become a popular approach in the de-
sign and development of complex safety-critical systems. Its primary advantage
lies in the “divide and conquer” strategy to address the inherent complexities
of CPSs, thereby enhancing both the efficiency and reliability of system de-
sign. This strategy is embodied through two dimensions: horizontal composi-
tion/decomposition and vertical abstraction/refinement. In the horizontal di-
mension, MBD facilitates the integration of heterogeneous models, resulting in
modeling techniques with heightened expressive capabilities. For example, AADL
models and Simulink/Stateflow models can be composed at the graphical mod-
eling level [25], leveraging each other’s strengths. In the vertical dimension, it
supports the analysis of models at different levels of abstraction, ranging from
intuitive graphical models to rigorous formal models [10], and ultimately to ex-
ecutable code [21]. By adhering to the orthogonal design principles, MBD effec-
tively alleviates the complexity of system modeling, ensuring a more manageable
and robust development process.

However, we observe a lake of dedicated modeling and analysis methods for
mobile CPSs. As complex heterogeneous systems, mobile CPSs integrate discrete
computational, control, and communication processes while deeply embedding
the continuous evolution of the physical world. In the context of mobile comput-
ing, these systems must consider the openness, uncertainty, and variability of the
context, including challenges posed by device diversity, network dynamics, and
resource constraints. These characteristics impose significant hurdles for effec-
tively modeling CPSs. Moreover, in mobile computing, the entities interacting
with the system exhibit heterogeneity and diverse interaction modalities, result-
ing in intricate causality chains that may alter safety. Capturing the complex be-
haviors of such systems accurately and comprehensively represents a formidable
challenge. Current modeling techniques, however, often adopt a narrower focus
on either hybrid behavior modeling or on mobile computing and communication,
which limits their ability to capture such intricate interactions and dynamic evo-
lution within the system and between the system and its environment.
To address these challenges, we propose an extension of sequence diagrams, as used in SysML/UML, to enable accurate and intuitive graphical representations of complex, deeply coupled mobile, parallel, and hybrid behaviors—specifically, the entangled interplay between discrete and continuous dynamics. To ensure the correctness of the designed model, we introduce a set of transformation rules that convert the extended sequence diagram—which is graphical and inherently informal—into a formal representation based on the hybrid π-calculus [23], a recently proposed formalism capable of capturing deeply coupled mobile, parallel, and hybrid behaviors of mobile CPSs. This formalization facilitates verification and analysis of the modeled system.

We start by introducing the preliminaries on sequence diagrams and the hy-
brid π-calculus in Section 2. Section 3 presents the extended sequence diagrams
and Section 4 translates the extended sequence diagram to the hybrid π-calculus.
The case study is shown in Section 5. Finally, Section 6 reviews related works and
positions our contributions accordingly, followed by the conclusion in Section 7.

2 Preliminaries

## 2.1 Sequence Diagrams

Sequence diagrams are used to depict the process of message passing and col-
laboration among system components over time. They include core elements
such as lifelines, messages, and combined fragments. Lifelines represent individ-
ual instances participating in an interaction by exchanging messages with other
lifelines. Time progresses downward along a lifeline, such that events occurring
higher up happen before those lower down on the same lifeline. Messages serve as
the fundamental units of communication between lifelines. Combined fragments
provide a mechanism to express control logic within interactions. Among them,
option, alternative, loop, and parallel are the most commonly used in practice.
The alt fragment represents conditional branching, similar to an if-then-else
construct. The opt fragment denotes optional execution of a single branch, akin
to an if statement without an else. The loop fragment indicates repeated
execution of a specific interaction sequence. The par fragment specifies parallel
execution of multiple interaction branches. We also consider break and critical
fragments. A break fragment represents an interruption of the normal flow in
order to execute an exceptional sequence, such as error handling. A critical
region denotes a section of interaction that must be executed atomically.

## 2.2 Hybrid π-Calculus

The hybrid π-calculus [23], as a conservative extension to Robin Milner et al.'s
traditional π-calculus [15], can formally capture both mobile computing and com-
munication as well as hybrid behavior in infrastructures where the network topol-
ogy and its communicating entities evolve continuously in the physical world.

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\pi ::= \tau & (\text{Silent}) & \mathbf{P} ::= \sum_{i \in I} \pi_i \cdot \mathbf{P}_i & (\text{Sum}) \\
| x(\mathbf{y}) & (\text{Input}) & | (\nu x)\mathbf{P} & (\text{Restriction}) \\
| \bar{x}\langle e \rangle & (\text{Output}) & | \mathbf{P} \parallel \mathbf{P}' & (\text{Parallel}) \\
| [B] & (\text{Guard}) & | !\mathbf{P} & (\text{Replication}) \\
| \{e_0 \mid \dot{v} = e \& B, \mathcal{R}\}(\mathbf{y}) & (\text{Continuous}) & &
\end{array}
$$

The syntax of the hybrid π-calculus consist of prefixes π and processes P. A sum ∑ i∈I πᵢ·Pᵢ represents a non-deterministic choice, where sub-terms guard a process Pᵢ by a prefix πᵢ, which can be a silence τ, an input x(y), an output x̄⟨e⟩, a Boolean clause [B], or a continuous clause {e₀ | v̇ = e&B, R}(y). The empty sum (I = ∅) stands for inaction and is written as process 0. The restriction of a name x to the scope of P is denoted (νx)P and subject to we adopt Barendregt's conventions. Replication is denoted by !P and parallel composition by P||P'. The term {e₀ | v̇ = e&B, R}(y).P denotes a continuous process. From left to right, it consists of a vector of expressions e₀ representing the initial state of the ODE's variables v and e its vector field which we require to be locally Lipschitz-continuous. The Boolean condition B defines the domain constraints (range or boundary) on the continuous variable. Once B is violated by the state of the ODE, e.g., c, its evolution stops immediately and its continuation (y).P is applied to the final state c, reducing to P{c/y}. We omit (y) if y are not free in the continuation P. Finally, the set R ⊆ {v, v̄ | v ∈ v} is called the ready set or interface of the ODE. It declares the channel names which can be sensed or actuated by discrete processes. We omit B if it is true and omit R if it is ∅.

3 Extended Sequence Diagrams

Interactions and activities in sequence diagrams are typically described using
informal methods such as natural language. This section aims to refine these in-
formal descriptions into more formal representations. Overall, these refinements
include: assignment (Section 3.1), communication (Section 3.2), continuous evo-
lution (of the physical environment, Section 3.3), sensation and actuation (inter-
actions between controlling processes and the physical environment, Section 3.4),
and timing constraints (Section 3.5). For clarity, we adopt PlantUML [18] to de-
scribe sequence diagrams, and the extension to sequence diagrams introduced in
this section will also be presented using PlantUML syntax (Section 3.6).

**3.1 Assignment**

Each participant **p** can assign values to its local variables: **p** → **p**: *x* := *e*, where *e* is an arithmetic expression evaluated and assigned to the variable *x*. For multiple assignments, we can employ the notation **p** → **p**: *x* := *e*, where *x* and *e* are vectors of variables. Note that assignments such **p** → **q**: *x* := *e*, where **p** ≠ **q**, are considered invalid, as it is generally not permissible for one participant to directly modify a variable belonging to another participant. Instead, such assignments
between participants can be facilitated through communication, which will be
detailed in the following discussion (Section 3.2).

## 3.2 Communication

Participants can interact through communication, which can be classified into two modes: synchronous and asynchronous. In synchronous communication, if one party is not ready to proceed, the other must wait. In contrast, asynchronous communication employs a buffer or queue between the sender and receiver. In this paper, we focus on synchronous communication: $p \to q: ch(x := e)$, where $p \neq q$. It specifies that participant $p$ sends expressions $e$ to participant $q$ via channel $ch$, while $q$ receives them through the same channel, storing them in variables $x$. This implies that vectors $x$ (used for reception) and $e$ (sent) must have the same length.

It is worthy noting that messages transmitted over a channel can themselves be channels (higher-order communication). For example, $p \to q: ch(x := ch')$ signifies that participant $p$ transfers ownership of channel $ch'$ to participant $q$. Afterward, $q$ can communicate with other participants via $ch'$, a mechanism referred to as mobile communication. Such higher-order communication is prevalent in mobile CPSs.

## 3.3 Continuous Evolution

In CPSs, physical entities, such as trains, undergo continuous evolution, which is typically modeled using ODEs. Therefore, we extend sequence diagrams by introducing ODEs. Concretely, the continuous evolution of a physical entity (participant) $p$ is modeled as an activity, referred to as a continuous activity, annotated (note) with an ODE, as shown below:

activate p
note Loc of p : «ode» {$e_0 | \dot{v} = e \& B$}
Frag
deactivate p

where $Loc ::= \text{left} | \text{right} | \text{over}$ denotes the position of the ODE relative to the activity in the diagram, and $Frag$ contains the interactions (sensation and actuation in Section 3.4) of $p$ with other participants. In this context, participants performing continuous evolution are referred to as *physical participants*, whereas those interacting with physical participants are termed *discrete participants*.

The above notation specifies that participant $p$ activates a continuous evolution described by {$e_0 | \dot{v} = e \& B$}, where the physical variables $v$ start from the initial condition $e_0$ and evolve according to the ODE $\dot{v} = e$. Once the evolution reaches the boundary of $B$, i.e., the boundary condition $B$ is violated, the evolution terminates, i.e., the continuous evolution is deactivated.

After the deactivation, we use $v'$ to represent the values of the physical variables $v$ at the termination of the ODE. For example, $p \to q: ch(x := v')$
after **deactivate p** means that **p** sends the final values of the ODE to **q** via channel **ch**; and **note Loc of p** : «**ode**» {*v*′ | **v**′ = **e**′&**B**′} after **deactivate p** indicates that **p** has activated another continuous evolution starting from the final values (*v*′) of the preceding one.

## 3.4 Sensation and Actuation

As discussed in Section 3.3, physical participants may interact with discrete participants during their continuous evolution. Specifically, a discrete participant may sense (read) and/or actuate (write) certain physical variables of a physical participant to perform the control. For example, a base station can read the real-time position and velocity of a train (sensation) within its coverage area and subsequently adjust the train's acceleration (actuation) based on the sensed data to ensure safety. Therefore, we extend sequence diagrams by introducing two types of interactions: sensation and actuation.

Sensation is modeled using the following notation: $p \to q : \langle \text{sense} \rangle x := v$, where $p \neq q$. It specifies that participant **p** senses the current value of the physical variable **v** of participant **q** and stores the sensed value in variable **x**. This indicates that **p** is a discrete participant while **q** is a physical one. Actuation is similarly modeled as: $p \to q : \langle \text{actuate} \rangle v := e$. This indicates that **p** modifies the value of the physical variable **v** to **e**.

## 3.5 Delay

In plant-control models, the control component typically operates periodically. For example, a train's controller may periodically read its state (sensation) and perform corresponding actions to regulate its motion (actuation). This periodic behavior can be effectively captured using delay constructs, which may occur within specific loops. In an extended sequence diagram, delay behaviors can be represented using a **delay** activity, defined by **activate p note Loc of p:delay(d) deactivate p** to mean that participant **p** delays for **d** time units.

## 3.6 Syntax of Extended Sequence Diagrams

Each ESD starts with @startuml and ends with @enduml. The interactions are structured using Fragments, which can include basic operations (assignment, communication, sensation, and actuation), continuous activities, alternatives, options, loops, breaks, parallel compositions, and critical regions. Additionally, to enhance the expressiveness of the model, we extend each alternative with an index [*i*] and a participant **p** responsible for evaluating the *condition*. Concretely, the fragment `alt[i] p: cond Frag else Frag' end` means that this is the *i*-th *alt* fragment and the evaluation of its *cond* is performed by **p**. In other words, **p** selects the branch of the *alt* fragment to execute, while the index [*i*] distinguishes different *alt* fragments. Similarly, we extend *opt* and *loop* by adding an index [*i*] and associating them with a participant **p**.
In summary, the PlantUML syntax of the extended sequence diagram (ESD) is specified by the following grammar:

```
ESD ::= @startuml Frag @enduml
Frag ::= ∅ | p → p : x := e Frag | p → q : ch(x := e) Frag
        | p → q : «sense» x := v Frag | p → q : «actuate» v := e Frag
        | activate Note p Frag deactivate p Frag
        | alt[i] p : cond Frag ALT | opt[i] p : cond Frag end Frag
        | loop[i] p : cond Frag end Frag | break Frag end
        | par Frag PAR | critical Frag end Frag
ALT ::= else Frag end Frag | else cond Frag ALT
PAR ::= else Frag end Frag | else Frag PAR
Note ::= note Loc of p : «ode» {e₀ | ˙v = e&B}
        | note Loc of p : delay(d)
Loc ::= left | right | over
```

# 4 Translation to Hybrid π-Calculus

Sequence diagrams serve as graphical models that enable users to model systems intuitively. However, ensuring the correctness of established models poses a significant challenge. By transforming these informal models into formal ones, we enable formal verification based on rigorous mathematical theories, which ensures the safety and reliability of system models. Among numerous formal methods, hybrid π-calculus stands out for its ability to represent both the hybrid behavior and the mobile communication (higher-order communication, Section 3.2) of CPSs. Therefore, this section presents the rules for translating extended sequence diagrams into hybrid π-calculus processes.

Specifically, the translation can be represented as a function $\mathcal{T}(\text{ESD}) = \mathbf{P}$, where ESD denotes an extended sequence diagram and $\mathbf{P}$ represents the corresponding hybrid π-calculus process for ESD, i.e., the formal representation of ESD. To define the translation function $\mathcal{T}$, we introduce an auxiliary function $\mathcal{T}(\text{Frag}, \mathcal{P}) = \{p : \mathbf{P}_p\}_{p \in \mathcal{P}}$, which takes a Fragment of the ESD as input, and outputs a mapping $\{p : \mathbf{P}_p\}_{p \in \mathcal{P}}$, where $\mathcal{P}$ is the set of all the participants involved in the ESD. The function $\mathcal{T}$ is defined through a set of transformation rules. We begin with the base case in which the interaction fragment is empty. In this case, each participant performs no action, denoted by the inaction $\mathbf{O}$, i.e., $\mathcal{T}(\emptyset, \mathcal{P}) = \{p : \mathbf{O}\}_{p \in \mathcal{P}}$. The remaining translation rules are presented below. All of them have been implemented in Python$^4$.

## 4.1 Assignment

For an assignment prefixed fragment, denoted $q \rightarrow q : x := e Frag$, if the hybrid π-calculus process of each participant can be derived from Frag, then the

<footnote n="4">⁴ https://github.com/Jixiang-Miao/ESD-to-HpC</footnote>
assignment is added as the prefix to the process $P_q$ of the participant $q$:

$$ \frac{\mathcal{T}(\text{Frag}, \mathcal{P}) = \{\text{p} : P_{\text{p}}\}_{\text{p}\in\mathcal{P}}}{\mathcal{T}(\text{q} \to \text{q} : x := e \text{ Frag}, \mathcal{P}) = \{\text{q} : \langle x := e \rangle.P_{\text{q}}\} \cup \{\text{p} : P_{\text{p}}\}_{\text{p}\in\mathcal{P}\setminus\text{q}}} $$

Since the hybrid π-calculus does not include an assignment operation, we introduce $\langle x := e \rangle$ as syntactic sugar for assignments in this section. We first define an auxiliary process Memory to manage the storage of the variable $x$, initialized to a value $y$:

$$ \text{Memory} \triangleq !a(y).(\overline{x'}\langle y \rangle.\overline{a}\langle y \rangle + x'(z).\overline{a}\langle z \rangle) $$

A hybrid π-calculus process can “activate” a Memory location by invoking $\overline{a}\langle e \rangle$. This renders a behavior similar to allocating a space in memory for the variable $x$ and to storing the value $e$ into it. Subsequently, the process can read the value of $x$ from the “memory” using $x'(x)$, and it can also store a new value $e'$ into $x$ using $\overline{x'}\langle e' \rangle$. Here is an example illustrating the operations “allocation”, “load”, and “store” on the Memory:

$$ \begin{align*} \overline{a}\langle e \rangle \cdot x'(x) \cdot \overline{x'}\langle x + 1 \rangle &\parallel \text{Memory} \to x'(x) \cdot \overline{x'}\langle x + 1 \rangle \parallel (\overline{x'}\langle e \rangle \cdot \overline{a}\langle e \rangle + x'(z) \cdot \overline{a}\langle z \rangle) \parallel \text{Memory} \\ &\to \overline{x'}\langle e + 1 \rangle \parallel (\overline{a}\langle e \rangle \parallel \text{Memory} \\ &\to \overline{x'}\langle e + 1 \rangle \parallel (\overline{x'}\langle e \rangle \cdot \overline{a}\langle e \rangle + x'(z) \cdot \overline{a}\langle z \rangle) \parallel \text{Memory} \\ &\to \overline{a}\langle e + 1 \rangle \parallel \text{Memory} \\ &\to (\overline{x'}\langle e + 1 \rangle \cdot \overline{a}\langle e + 1 \rangle + x'(z) \cdot \overline{a}\langle z \rangle) \parallel \text{Memory} \end{align*} $$

Given a hybrid π-calculus process P containing assignments, the first occurrence of an assignment $\langle x := e \rangle$ should hence be replaced with $\overline{a}\langle e \rangle$, while subsequent assignments $\langle x := e' \rangle$ should be replaced with $\overline{x'}\langle e' \rangle$. Then, a “load” operation for $x$, denoted $x'(x)$, must be inserted before every free occurrence of $x$ in the process. This transformation is formally captured by the function $A_x$. Consequently, any process P that only contains assignments to the variable $x$ is equivalent to $(\nu a, x')$ ($A_x(P) \parallel \text{Memory}$), where $(\nu a, x')$ indicates that the names $a$ and $x'$ are bound and therefore hidden (or inaccessible) from the environment.

## 4.2 Communication

The communication prefix $q \to q' : ch(x := e)$ indicates that participant $q$ sends expressions $e$ to participant $q'$ via channel $ch$. Consequently, the corresponding process prefix for $q$ is $\overline{ch}\langle e \rangle$. Participant $q'$ receives the expressions from channel $ch$ and stores them to variables $x$. Therefore, the corresponding process prefix is $ch(x)$. This is illustrated by the following rule:

$$ \frac{\mathcal{T}(\text{Frag}, \mathcal{P}) = \{\text{p} : P_{\text{p}}\}_{\text{p}\in\mathcal{P}}}{\mathcal{T}(\substack{\text{q} \to \text{q} : ch(x := e) \\ \text{Frag}}), \mathcal{P}) = \{\text{q} : \overline{ch}\langle e \rangle.P_{\text{q}}, \text{q}' : ch(x).P_{\text{q}'}\} \cup \{\text{p} : P_{\text{p}}\}_{\text{p}\in\mathcal{P}-\{\text{q}, \text{q}'\}}} $$
## 4.3 Continuous Evolution

As described in Section 3.3, the continuous evolution of physical participants is modeled as continuous activities:

activate q note Loc of q: «ode» {$e_0 | \dot{v} = e \& B$} Frag deactivate q

where physical participant q evolves according to the ODE {$e_0 | \dot{v} = e \& B$}, and the interaction fragment Frag contains the sensation and actuation between this ODE and discrete participants. Therefore, we first analyze the interactions of participant q within Frag to compute the ready set of its ODE (see Section 2.2 for details). This ready set defines the interface through which the ODE interacts with discrete participants. The computation of the ready set is formalized as a function $\Re(q, Frag) = \mathcal{R}$. Specifically, If q is not involved in the interactions of Frag, the corresponding ready set is empty: $\Re(q, \emptyset) = \emptyset$. If a physical variable v of q is sensed by some discrete participant, the corresponding output action $\bar{v}$ is included in the ready set. Symmetrically, if a physical variable v of q is actuated by a discrete participant, the corresponding input action v is included in the ready set.

Based on the aforementioned ready set construction rules, continuous activities can be translated according to the following rule:

$$ \mathcal{R} = \Re(q, Frag) \cap \{v, \bar{v} | v \in v\} \quad \mathcal{T}(Frag, Frag', P) = \{p : P_p\}_{p \in P} \\ \left( \begin{array}{l} \text{activate q} \\ \text{note Loc of q:} \\ \text{«ode» } \{e_0 | \dot{v} = e \& B\}, P \\ \text{Frag} \\ \text{deactivate q} \\ \text{Frag'} \end{array} \right) = \left( \begin{array}{l} \{q : \{e_0 | \dot{v} = e \& B, \mathcal{R}\}(v').P_q\} \\ \cup \\ \{p : P_p\}_{p \in P \setminus q} \end{array} \right) $$

where $v'$ denote the values of the physical variables $v$ at the termination of the ODE. The premise $\mathcal{R} = \Re(q, Frag) \cap \{v, \bar{v} | v \in v\}$ indicates that the ready set $\mathcal{R}$ forms a valid interface for the ODE {$e_0 | \dot{v} = e \& B$}.

## 4.4 Sensation and Actuation

The sensation prefix $q \to q'$: «sense» $x := v$ indicates that participant q reads the current value of the physical variable $v$ from participant $q'$ and assigns it to variable $x$. Consequently, the prefix of the process corresponding to q is $v(x)$, leading to the following rule:

$$ \mathcal{T}(Frag, P) = \{p : P_p\}_{p \in P} \\ \mathcal{T}\left(\begin{array}{l} q \to q' : \text{«sense»} x := v, P \\ \text{Frag} \end{array}\right) = \{q : v(x).P_q\} \cup \{p : P_p\}_{p \in P \setminus q} $$

where participant $q' \in P \setminus q$ is a physical participant, and its translation rules were introduced in Section 4.3.
The actuation prefix $q \to q' : \text{«actuate»} v := e$ is dual to the sensation prefix above. It indicates that participant $q$ updates the value of the physical variable $v$ of the physical participant $q$ to $e$, leading to the following rule:

$$ \frac{\mathcal{T}(\text{Frag}, \mathcal{P}) = \{\text{p} : \text{P}_{\text{p}}\}_{\text{p} \in \mathcal{P}}}{\mathcal{T}\left(\substack{\text{q} \to \text{q}': \text{«actuate»} v := e \\ \text{Frag}}\right) = \{\text{q} : \bar{v}\langle e \rangle \cdot \text{P}_{\text{q}}\} \cup \{\text{p} : \text{P}_{\text{p}}\}_{\text{p} \in \mathcal{P}\setminus\text{q}}} $$

## 4.5 Delay

The delay activity of participant $q$ is translated to a wait prefix:

$$ \frac{\mathcal{T}(\text{Frag}, \mathcal{P}) = \{\text{p} : \text{P}\}_{\text{p} \in \mathcal{P}}}{\mathcal{T}\left(\substack{\text{activate } \text{q} \\ \text{note Loc of } \text{q} : \text{delay}(d), \mathcal{P} \\ \text{deactivate } \text{q} \\ \text{Frag}}\right) = \{\text{q} : \text{wait}(d) \cdot \text{P}_{\text{q}}\} \cup \{\text{p} : \text{P}_{\text{p}}\}_{\text{p} \in \mathcal{P}\setminus\text{q}}} $$

where notation wait(d) $\triangleq$ (vt){0 | $\dot{t}$ = 1&t < d} is syntactic sugar for representing delay in the hybrid $\pi$-calculus (Section 2.2).

## 4.6 Alternative

For the sake of clarity, the alt fragment considered in this section only includes two branches, mirroring an if-then-else structure, and the method can naturally be extended to alt fragments with more branches. Suppose that the condition cond of the alt fragment is evaluated by participant $q$. Based on the result of this evaluation, $q$ sends corresponding signals to other participants within the fragment, thereby scheduling them to perform interactions in either the true or false branch.

It is important to note that $q$ should not schedule physical participants, but it can schedule the interactions of those discrete participants to sense and actuate physical participants in different alt branches. We define a function DisP that takes an interaction fragment Frag as input and returns the set of all discrete participants involved in Frag. This leads to the following rule:

$$ \frac{\mathcal{T}(\text{Frag}, \text{Frag}'', \mathcal{P}) = \{\text{p} : \text{P}_{\text{p}}\}_{\text{p} \in \mathcal{P}}}{\text{DisP}(\text{Frag}) = \text{P}} \quad \mathcal{T}(\text{Frag}', \text{Frag}'', \mathcal{P}) = \{\text{p} : \text{P}'_{\text{p}}\}_{\text{p} \in \mathcal{P}} \\ \text{DisP}(\text{Frag}') = \text{P}' \quad \text{P} \cup \text{P}' = \{\text{q}, \text{p}_1, \dots, \text{p}_k\} $$

$$ \mathcal{T}\left(\substack{\text{alt}[i] \text{ q} : \text{cond} \\ \text{Frag} \\ \text{else} \\ \text{Frag}' \\ \text{end} \\ \text{Frag}''} , \mathcal{P}\right) = \left\{ \substack{\text{q} : \left( \substack{\text{if cond then} \\ \overline{\text{alt}_{i,1}} \dots \overline{\text{alt}_{i,k}} \cdot \text{P}_{\text{q}}} \\ \text{else} \\ \overline{\text{alt}'_{i,1}} \dots \overline{\text{alt}'_{i,k}} \cdot \text{P}'_{\text{q}}} \right) \\ \cup \\ \{\text{p}_j : \text{alt}_{i,j} \cdot \text{P}_{p_j} + \text{alt}'_{i,j} \cdot \text{P}'_{p_j}\}_{1 \le j \le k} \\ \cup \{\text{p} : \text{P}_{\text{p}}\}_{\text{p} \in \mathcal{P} - (\text{P} \cup \text{P}') \} \end{substack}} \right\} $$
where notation if B then P else Q $\triangleq$ [B].P + [¬B].Q is syntactic sugar of conditional in the hybrid π-calculus (Section 2.2).

Participant q evaluates the value of the Boolean expression cond. If the result is true, it schedules (via $\overline{\text{alt}}_{i,j}$) the interactions of other discrete participants $p_i$ in Frag Frag'' (denoted $P_{p_j}$), where $1 \le j \le k$, and then executes its own interactions in Frag Frag'' (denoted $P_q$). Otherwise (if false), it schedules (via $\overline{\text{alt}}'_{i,j}$) the interactions of $p_j$ in Frag' Frag'' (denoted $P'_{p_j}$), and then executes its own interactions in Frag' Frag'' (denoted $P'_q$).

## 4.7 Option

An opt fragment is a special case of an alt fragment, analogous to the if-then construct. Formally, $\mathcal{T}(\text{opt}[i] \ q: \text{cond} \ Frag \ end \ Frag', \mathcal{P})$ is equivalent to

$$ \mathcal{T}(\text{alt}[i] \ q: \text{cond} \ Frag \ \text{else} \ \emptyset \ \text{end} \ Frag', \mathcal{P}) $$

## 4.8 Loop

Assume that the condition cond of the loop fragment is evaluated by participant q. Similar to the alt fragment discussed in Section 4.6, q can only schedule the interactions of discrete participants within the loop fragment, but not those of physical participants. This leads to the following translation rule:

$$ \begin{gathered} \mathcal{T}(\text{Frag}, \mathcal{P}) = \{\mathbf{p} : P_{\mathbf{p}}\}_{\mathbf{p} \in \mathcal{P}} \quad \mathcal{T}(\text{Frag}', \mathcal{P}) = \{\mathbf{p} : P'_{\mathbf{p}}\}_{\mathbf{p} \in \mathcal{P}} \\ \text{DisP}(\text{Frag}) = P = \{\mathbf{q}, p_1, \dots, p_k\} \end{gathered} $$

$$ \mathcal{T} \left( \begin{array}{c} \text{loop}[i] \quad \mathbf{q} : \text{cond} \\ \text{Frag} \\ \text{end} \\ \text{Frag}' \end{array} , \mathcal{P} \right) = \left\{ \mathbf{q} : \mu \text{loop}_i . \left( \begin{array}{c} \text{if } \text{cond} \ \text{then} \\ \overline{\text{loop}}_{i,1} . \dots . \overline{\text{loop}}_{i,k} . P_{\mathbf{q}} . \overline{\text{loop}}_i \\ \text{else} \\ \overline{\text{loop}}'_{i,1} . \dots . \overline{\text{loop}}'_{i,k} . P'_{\mathbf{q}} \end{array} \right) \right\} \\ \cup \{\mathbf{p}_j : ! (\overline{\text{loop}}_{i,j} . P_{\mathbf{p}_j} + \overline{\text{loop}}'_{i,j} . P'_{\mathbf{p}_j})\}_{1 \le j \le k} \\ \cup \{\mathbf{p} : P_{\mathbf{p}}\}_{P \neq P} $$

where $\mu x(y).P@\langle e \rangle \triangleq (\nu x)(\bar{x}\langle e \rangle \|!x(y).P)$ is syntactic sugar for expressing recursion in the hybrid π-calculus (Section 2.2), and particularly, $\mu x.P \triangleq \mu x().P@\langle \cdot \rangle$.

At each iteration, participant q checks whether the condition cond holds. If true, it schedules (via $\overline{\text{loop}}_{i,j}$) the interactions of other discrete participants $p_j$ within the loop body Frag (denoted $P_{p_j}$), where $1 \le j \le k$. After that, it executes its own interactions within the loop body (denoted $P_q$) and initiates the next iteration of the loop (via $\overline{\text{loop}}_i$). Otherwise, it schedules (via $\overline{\text{loop}}'_{i,j}$) the interactions of $p_j$ in Frag' (denoted $P'_{p_j}$), indicating the end of the loop. It then proceeds to execute its own post-loop interactions, denoted $P'_q$.

When translating a break fragment nested inside a loop, the containing loop fragment, denoted $\text{loop}[i] \ q: \text{cond} \ Frag \ end$, must first be modified as follows:

- Insert the assignment $\mathbf{q} \to \mathbf{q} : break_i := 0$ immediately before the loop;

- Update the loop condition to $\text{cond} \land break_i = 0$;
– Append the assignment $q \to q: break_i := 1$ right after the **break** fragment.

After these modifications, the following translation rule applies:

$$T(\text{break Frag end Frag}', \mathcal{P}) = T(\text{Frag}, \mathcal{P})$$

## 4.9 Parallel

The **par** fragment in sequence diagrams reflects interleaving: interactions within the same fragment must preserve their order, whereas those in different parallel fragments may occur in any order. Therefore, we assume that the **par** fragment does not involve physical participants, since parallel continuous behaviors are typically executed synchronously rather than in an interleaved manner.

Similar to the **alt** fragment introduced in Section 4.6, we consider for clarity the parallel composition of only two fragments; however, the approach can naturally be extended to cases involving multiple parallel fragments. Additionally, we assume that each **par** fragment is composed of assignments (Sections 3.1 and 4.1), communications (Sections 3.2 and 4.2), and **critical** regions. These **critical** fragments may also include more complex structures, such as nested **alt**, **loop**, or even sub-**par** fragments.

We define the auxiliary function $T_1$, which selects the first interaction of the first **par** fragment to execute, and then returns the translation result based on this selection. Concretely,

$$T_1(\text{par } \emptyset \text{ else Frag end Frag}', \mathcal{P}) = T(\text{Frag Frag}', \mathcal{P})$$

$$T_1(\text{par } \textcolor{red}{p} \to \textcolor{red}{p}: x := e \text{ Frag else Frag}' \text{ end Frag''}, \mathcal{P}) = T(\textcolor{red}{p} \to \textcolor{red}{p}: x := e \text{ par Frag else Frag}' \text{ end Frag''}, \mathcal{P})$$

$$T_1(\text{par } \textcolor{red}{p} \to \textcolor{red}{q}: ch(x := e) \text{ Frag else Frag}' \text{ end Frag''}, \mathcal{P}) = T(\textcolor{red}{p} \to \textcolor{red}{q}: ch(x := e) \text{ par Frag else Frag}' \text{ end Frag''}, \mathcal{P})$$

$$T_1(\text{par critical Frag end Frag' else Frag'' end Frag'''}, \mathcal{P}) = T(\text{critical Frag end par Frag' else Frag'' end Frag'''}, \mathcal{P})$$

If the first fragment is empty, i.e., par $\emptyset$ else Frag end (i.e., a case without any parallel structure), this simplifies to just Frag. If the first fragment is a **critical** region, the interactions within the region should be executed atomically. Based on $T_1$, the translation rule for **par** fragments is given as follows:

$$\frac{T_1(\text{par Frag else Frag' end Frag''}, \mathcal{P}) = \{\textcolor{red}{p}: \mathcal{P}\}_{\mathcal{P} \in \mathcal{P}} \\ T_1(\text{par Frag' else Frag end Frag''}, \mathcal{P}) = \{\textcolor{blue}{p}: \mathcal{P}'\}_{\mathcal{P}' \in \mathcal{P}} \\ T(\text{par Frag else Frag' end Frag''}, \mathcal{P}) = \{\textcolor{blue}{p}: \mathcal{P} + \mathcal{P}'\}_{\mathcal{P} \in \mathcal{P}}$$

The function $T_1(\text{par Frag else Frag' end Frag''}, \mathcal{P})$ returns the translation result obtained by selecting the first interaction (or the first **critical** region) of the **Fragment**. Similarly, $T_1(\text{par Frag' else Frag end Frag''}, \mathcal{P})$ returns the translation result of selecting the first interaction (or the first **critical** region) of the **Frag'**. Combining these two results with the nondeterministic choice operator (+) reflects the interleaving nature of the **par** fragment.
It is important to ensure that both operands of the + operator are in the form of a sum. Specifically, if both P and P' are already sums (i.e., represented as $\sum_{i \in I} \pi_i.P_i$), then P + P' directly forms a sum; if P is a sum but P' is not, a silent prefix $\tau$ should be added to P', resulting in $P + \tau.P'$; if P' is a sum but P is not, the prefix $\tau$ should instead be added to P, yielding $\tau.P + P'$; finally, if neither P nor P' is a sum, both must be prefixed with $\tau$, leading to $\tau.P + \tau.P'$.

## 4.10 Start and End

The start marker (@startuml) and end marker (@enduml) denote a complete ESD, i.e., ESD ::= @startuml Frag @enduml, according to the syntax in Section 3.6. If the hybrid $\pi$-calculus processes for each participant can be derived from the Frag, i.e., $\mathcal{T}(\text{Frag}, \{p_1, \dots, p_n\}) = \{p_1 : P_1, \dots, p_n : P_n\}$, then the hybrid $\pi$-calculus process of the ESD is the parallel composition of all $P_i$s:

$$ \frac{\mathcal{T}(\text{Frag}, \{p_1, \dots, p_n\}) = \{p_1 : P_1, \dots, p_n : P_n\}}{\mathcal{T}(\text{@startuml Frag @enduml}) = P_1 \| \dots \| P_n} $$

## 5 Case Study

We model a successful handover scenario of the train control system's protocol, as introduced in [23], using the extended sequence diagram proposed in Section 3. We then formalize this model into a hybrid $\pi$-calculus process, adhering to the translation rules specified in Section 4. The scenario involves two adjacent track sectors and a train. Initially, the train is positioned at the starting point of the left sector and moves under its control. The left sector periodically reads the train's real-time position and velocity (sensation) and, based on this information, computes an acceleration. This newly computed acceleration is then sent to the train (actuation) to regulate its continuous movement. The train's motion is governed by a set of ODEs, until it arrives at the terminus.

Upon reaching the handover point of the left sector, the left sector initiates a handover request to the right sector. In this scenario, we assume that the right sector is available and thus responds with "yes". Subsequently, the left sector transfers the train's physical variables—position ($p$), velocity ($v$), and acceleration ($a$)—to the right sector. At this point, the handover is successfully concluded, and the right sector assumes control of the train using the received variables. In essence, the control of the train is transferred from the left sector to the right one (mobility). Similarly, the right sector will periodically sense and actuate the train until it reaches the handover point of the right sector. At this juncture, the right sector sets the train's acceleration to $-1 \text{ m/s}^2$, causing it to come to a stop before reaching the end of the right sector. The extended sequence diagram for this scenario is illustrated in Fig. 1, where the control periods for both the left and right sectors are set to 1 second, and the control algorithm is denoted by the function $f$.

The function $f$ takes as inputs the real-time position ($p_0$) and velocity ($v_0$) of the train, along with the endpoint of the sector containing the train, and outputs
<figure><img src="image_2.png" /><figcaption>Fig. 1. The ESD of the successful handover scenario in PlantUML.</figcaption></figure>
a safe acceleration for the train. More specifically, $f$ first checks whether it is safe for the train to run at the maximum acceleration (1 m/s²) during the next control period (1 second). If so, it outputs the maximum acceleration. Otherwise, it checks whether it is safe for the train to maintain its current speed. If this is safe, it outputs 0. Otherwise, it outputs a deceleration of -1 m/s² to prevent the train from entering an unsafe region, i.e., crossing the *endpoint* of the current sector or exceeding the velocity limit of 40 m/s. Further details of the function $f$ can be found in the case study presented in [23, 24].

By applying the translation rules defined in Section 4, the hybrid π-calculus process of the extended sequence diagram in Fig. 1 is derived as follows:

$$
\begin{align*}
\text{System} &\triangleq \text{Train} \parallel \text{LeftSector} \parallel \text{RightSector} \\
\text{Train} &\triangleq \langle \text{terminus} := 10000 \rangle . \left\{ \begin{array}{@{}l@{}} 0 \mid \dot{p} = v \\ 0 \mid \dot{v} = a \ \& \ p < \text{terminus}, \{\bar{p}, \bar{v}, a\} \\ 0 \mid \dot{a} = 0 \end{array} \right\} \\
\text{LeftSector} &\triangleq \langle \text{handover\_point} := 4000 \rangle . \langle \text{endpoint} := 5000 \rangle . p(p_0) \\
&\qquad \mu \text{loop}_1 . \left( \begin{array}{@{}l@{}} \text{if } p_0 < \text{handover\_point} \ \text{then} \\ \quad v(v_0) . \langle a_0 := f(p_0, v_0, \text{endpoint}) \rangle . \bar{a}(a_0) . \\ \quad \text{wait}(1) . p(p_0) . \overline{\text{loop}_1} \\ \quad \text{else } \text{handover.yes channels}(p, v, a) \end{array} \right) \\
\text{RightSector} &\triangleq \langle \text{handover\_point} := 9000 \rangle . \langle \text{endpoint} := 10000 \rangle . \\
&\qquad \text{handover.} \overline{\text{yes channels}}(p_1, v_1, a_1) . p_1(p_0) \\
&\qquad \mu \text{loop}_2 . \left( \begin{array}{@{}l@{}} \text{if } p_0 < \text{handover\_point} \ \text{then} \\ \quad v_1(v_0) . \langle a_0 := f(p_0, v_0, \text{endpoint}) \rangle . \bar{a}_1(a_0) . \\ \quad \text{wait}(1) . p_1(p_0) . \overline{\text{loop}_2} \\ \quad \text{else } \bar{a}_1 \langle -1 \rangle \end{array} \right)
\end{align*}
$$

The System model serves as a formal representation of the informal graphical model illustrated in Fig. 1. For this formal model, some analysis and verification can be conducted. For instance, we can define the formal specification (SPEC) of this scenario using the hybrid π-calculus as follows:

$$
\begin{align*}
\text{SPEC} &\triangleq (\nu p, v) ((\text{ACC.Steady.DEC}) \parallel \text{Observer}) \\
\text{ACC} &\triangleq \{0, 0 \mid \dot{p} = v, \dot{v} = 1 \ \& \ p < 800\}(p_1, v_1) \\
\text{Steady} &\triangleq \{p_1, v_1 \mid \dot{p} = v, \dot{v} = 0 \ \& \ p < 9200\}(p_2, v_2) \\
\text{DEC} &\triangleq \{p_2, v_2 \mid \dot{p} = v, \dot{v} = 0 \ \& \ p < 10000\} \\
\text{Observer} &\triangleq \{0 \mid \dot{x} = v \ \& \ p < 10000\}
\end{align*}
$$

Since the handover is successful in this scenario, the train smoothly runs from the left sector to the right one, and its evolution consists of three stages: accelerating for 800 meters (ACC), then maintaining a Steady speed until it is 800 meters away from the terminus, and finally decelerating until it comes to a stop (DEC). An additional process, Observer, monitors the evolution of the train and calculates its location using a free variable $x$ by sensing the recorded velocity $v$ of the train without actuating the dynamics of the train.

We also use the Observer to observe dynamics of train. Specifically, we obtain $\text{System}' \triangleq (\nu p, v, a, \text{handover}, \text{yes}, \text{no}, \text{channels}, c)(\text{System} \parallel \text{Observer})$, where the
channels and variables we do not wish to observe are hidden using $v$, and we
can demonstrate that System' and SPEC are in some weak bisimulation, i.e.,
System' $\approx$ SPEC, following the method used in [23].

# 6 Related Works

Yoshida et al. [12, 3] use sequence diagrams informally to depict communica-
tion protocols in distributed systems, particularly in multiparty session types.
Although lacking formal semantics, these diagrams effectively illustrate interac-
tion structures and improve understanding, highlighting the potential for their
formalization to support rigorous analysis. Grosu et al. [9] introduced Hybrid
Sequence Charts (HySCs), which provide a synchronous semantic framework for
hybrid systems sharing time and continuous variables. However, HySCs have
limited expressiveness for complex continuous dynamics and may fail to capture
detailed system behaviors. Li et al. [13] proposed a formal semantics for UML
sequence diagrams by representing their abstract syntax as hierarchical trees and
defining a consistency-checking mechanism with class and state diagrams. This
approach, however, struggles with timing constraints and concurrency, limiting
its applicability in complex real-time systems. In terms of model transforma-
tion, several studies have translated sequence diagrams into executable or ana-
lyzable formal models, such as PROMELA [14], Timed Automata Network [11],
CCS [17], Petri nets [5] and Clock Constraint Specification Language [4], en-
abling formal verification. More recently, Zhao et al. [28] proposed KBX, a for-
mal bidirectional transformation (BX) framework for verified model synchro-
nization. As an application, they derive a BX between UML Sequence Diagrams
and HCSP by first specifying a unidirectional transformation from HCSP to
UML. However, their work only supports a limited subset of UML constructs
and lacks mobility. Xu et al. [25] proposed a framework that integrates AADL
with Simulink/Stateflow, referred to as AADL$\oplus$S/S, along with a method for
translating the combined model into HCSP. This translation enables subsequent
simulation and verification [20]. The verified HCSP model can then be trans-
lated into SystemC [26] and C [21]. Implemented as part of the toolchain MARS
2.0 [27], this framework supports the transformation from graphical AADL$\oplus$S/S
models to formal HCSP models, and ultimately to executable code. Our work
will extend this framework by adding SysML formal modeling and analysis for
broader industrial applicability.

In terms of verification tools, Vince et al. [16] leveraged five specialized tools
for SysML v2 formal analysis and verification. Each tool, already integrated with
SysML v2, employs distinct verification approaches (such as model checking and
theorem proving) targeting different verification objectives. David et al. [8] pro-
posed a method to formalize real-time extensions of UML state machine diagrams
into Hierarchical Timed Automata (HTA) and translate HTA into flat timed
automata for verification with UPPAAL. Rahim et al. [19] generated PNML
documents from activity diagrams and converted them into CPNTools models
to analyze safety and liveness properties. Lima et al. [14] implemented an auto-
matic translation from UML sequence diagrams to PROMELA, enabling simu-
lation and temporal property verification via the SPIN model checker. Similarly,
Messaoud et al. [1] used Zenon, an automated theorem prover in FoCaLiZe, to
verify formal models. Wu et al. [22] proposed simulating hybrid SysML models
within the DEVS framework, allowing engineers to perform verification using
DEVS-based tools without requiring deep expertise in DEVS theory, thereby
improving modeling and verification efficiency.

Our work presents the first extension of sequence diagrams of SysML/UML
with hybrid behavior and mobile communication, enabling them to model mobile
CPSs. Based on this extension, we translate the extended sequence diagrams into
the hybrid π-calculus models. In other words, we provide a formal semantics
for the extended sequence diagrams based on the hybrid π-calculus, thereby
supporting analysis and verification at the level of formal models. We plan to
integrate our work into the toolchain MARS 2.0 [27], supporting MBD for CPSs
in the context of mobile computing.

7 Conclusion and Future Works

In this paper, we proposed an extension of sequence diagrams in SysML/UML
to better capture the complex behaviors inherent in mobile CPSs, including mo-
bile computing and computation and hybrid behavior, i.e., the interplay between
discrete behavior and continuous dynamic. To ensure the correctness of safety-
critical systems modeled by the extended sequence diagram, we introduced a
set of transformation rules that translate the (graphical) extended sequence dia-
gram into a formal representation based on the hybrid π-calculus. This approach
bridges the gap between intuitive modeling and formal verification, supporting
the MBD paradigm that is essential for developing safe and reliable CPSs.

For future works, we intend to develop a simulator for the hybrid π-calculus.
This simulator will facilitate the visual observation of the execution of hybrid
π-calculus models generated from extended sequence diagrams, aiding in the
identification of potential flaws in the design of mobile CPSs. Additionally, we
aim to develop automatic or interactive provers for the hybrid π-calculus, thus
enabling formal verification of extended sequence diagrams. We will also inves-
tigate the code generation from (verified) hybrid π-calculus models, reflecting
the vertical dimension of MBD, i.e., the transformation from intuitive graphical
models to rigorous formal representations, and ultimately to executable code.

**Acknowledgments.** This work is funded by the Natural Science Foundation of China under grant No. 62402479, 62432005, 62192732, and the President's International Fellowship Initiative of the Chinese Academy of Sciences.

References

1. Abbas, M., Rioboo, R., Ben-Yelles, C., Snook, C.F.: Formal modeling and verification of UML activity diagrams (UAD) with FoCaLiZe. J. Syst. Archit. **114**, 101911 (2021). https://doi.org/10.1016/J.SYSARC.2020.101911
2. Bengler, K., Damm, W., Lüdtke, A., Rieger, J.W., Austel, B., Biebl, B., Fränzle, M., Hagemann, W., Held, M., Hess, D., Ihme, K., Kacianka, S., Kerscher, A.J., Laine, F., Lehnhoff, S., Pretschner, A., Rakow, A., Sonntag, D., Sztipanovits, J., Schwammberger, M., Schweda, M., Unni, A., Veith, E.M.S.P.: A references architecture for human cyber physical systems, part II: fundamental design principles for human-CPS interaction. ACM Trans. Cyber Phys. Syst. 8(1), 3:1–3:27 (2024). https://doi.org/10.1145/3622880

3. Bettini, L., Coppo, M., D'Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: International Conference on Concurrency Theory. pp. 418–433. Springer (2008)

4. Chen, X., Mallet, F., Liu, X.: Formally verifying sequence diagrams for safety critical systems. In: TASE 2020. pp. 217–224. IEEE (2020). https://doi.org/10.1109/TASE49443.2020.00037

5. Cunha, E., Custódio, M., Rocha, H., Barreto, R.S.: Formal verification of UML sequence diagrams in the embedded systems context. In: SBESC 2011. pp. 39–45. IEEE Computer Society (2011). https://doi.org/10.1109/SBESC.2011.18

6. Damm, W., Fränzle, M., Kerscher, A.J., Laine, F., Bengler, K., Biebl, B., Hagemann, W., Held, M., Hess, D., Ihme, K., Kacianka, S., Lehnhoff, S., Lüdtke, A., Pretschner, A., Rakow, A., Rieger, J.W., Sonntag, D., Sztipanovits, J., Schwammberger, M., Schweda, M., Trende, A., Unni, A., Veith, E.M.S.P.: A reference architecture of human cyber-physical systems - part III: semantic foundations. ACM Trans. Cyber Phys. Syst. 8(1), 4:1–4:23 (2024). https://doi.org/10.1145/3622881

7. Damm, W., Hess, D., Schweda, M., Sztipanovits, J., Bengler, K., Biebl, B., Fränzle, M., Hagemann, W., Held, M., Ihme, K., Kacianka, S., Kerscher, A.J., Lehnhoff, S., Lüdtke, A., Pretschner, A., Rakow, A., Rieger, J.W., Sonntag, D., Schwammberger, M., Austel, B., Unni, A., Veith, E.M.S.P.: A reference architecture of human cyber-physical systems - part I: fundamental concepts. ACM Trans. Cyber Phys. Syst. 8(1), 2:1–2:32 (2024). https://doi.org/10.1145/3622879

8. David, A., Möller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer (2002). https://doi.org/10.1007/3-540-45923-5_15

9. Grosu, R., Krüger, I., Stauner, T.: Hybrid sequence charts. In: ISORC 2000. p. 104. IEEE Computer Society (2000). https://doi.org/10.1109/ISORC.2000.839517

10. Guo, P., Zhan, B., Xu, X., Wang, S., Sun, W.: Translating a large subset of state-flow to hybrid CSP with code optimization. J. Syst. Archit. 130, 102665 (2022). https://doi.org/10.1016/J.SYSARC.2022.102665

11. Han, D., Xing, J., Yang, Q., Wang, H., Zhang, X.: Formal sequence: Extending UML sequence diagram for behavior description and formal verification. In: COMPSAC Workshops 2016. pp. 474–481. IEEE Computer Society (2016). https://doi.org/10.1109/COMPSAC.2016.118

12. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 273–284 (2008)

13. Li, X., Liu, Z., He, J.: A formal semantics of UML sequence diagram. In: ASWEC 2004. pp. 168–177. IEEE Computer Society (2004). https://doi.org/10.1109/ASWEC.2004.1290469

14. Lima, V., Talhi, C., Mouheb, D., Debbabi, M., Wang, L., Pourzandi, M.: Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. In: SSV 2009. ENTCS, vol. 254, pp. 143–160. Elsevier (2009). https://doi.org/10.1016/J.ENTCS.2009.09.064
15. Milner, R.: The polyadic π-calculus: a tutorial. In: Logic and Algebra of Specification. pp. 203–246. Springer Berlin Heidelberg, Berlin, Heidelberg (1993). https://doi.org/10.1007/978-3-642-58041-3_6

16. Molnár, V., Graics, B., Vörös, A., Tonetta, S., Cristoforetti, L., Kimberly, G., Dyer, P., Giammarco, K., Köthe, M., Hester, J., Smith, J., Grimm, C.: Towards the formal verification of SysML v2 models. In: MODELS (Companion) 2024. pp. 1086–1095. ACM (2024). https://doi.org/10.1145/3652620.3687820

17. Peng, T., Ding, G.: Formal specification and automated verification of UML2.0 sequence diagrams. In: GrC 2012. pp. 370–375. IEEE Computer Society (2012). https://doi.org/10.1109/GRC.2012.6468641

18. PlantUML Team: PlantUML. https://plantuml.com/en/

19. Rahim, M., Hammad, A., Boukala-Ioualalen, M.: Towards the formal verification of SysML specifications: Translation of activity diagrams into modular Petri nets. In: ACIT 2015. pp. 509–516. IEEE (2015). https://doi.org/10.1109/ACIT-CSI.2015.97

20. Sheng, H., Bentkamp, A., Zhan, B.: HHLPy: Practical verification of hybrid systems using Hoare logic. In: FM 2023. LNCS, vol. 14000, pp. 160–178. Springer (2023). https://doi.org/10.1007/978-3-031-27481-7_11

21. Wang, S., Ji, Z., Xu, X., Zhan, B., Gao, Q., Zhan, N.: Formally verified C code generation from hybrid communicating sequential processes. In: ICCPS 2024. pp. 123–134. IEEE (2024). https://doi.org/10.1109/ICCPS61052.2024.00018

22. Wu, X., Yan, X., Li, X., Wang, Y.: Simulating hybrid SysML models: a model transformation approach under the DEVS framework. J. Supercomput. **79**(2), 2010–2030 (2023). https://doi.org/10.1007/S11227-022-04654-6

23. Xu, X., Talpin, J., Wang, S., Wu, H., Zhan, B., Liu, X., Zhan, N.: HpC: A calculus for hybrid and mobile systems. Proc. ACM Program. Lang. **9**(OOPSLA1), 1158–1183 (2025). https://doi.org/10.1145/3720478

24. Xu, X., Talpin, J., Wang, S., Wu, H., Zhan, B., Liu, X., Zhan, N.: Hpc: A calculus for hybrid and mobile systems - full version. CoRR abs/2501.09430 (2025). https://doi.org/10.48550/ARXIV.2501.09430

25. Xu, X., Wang, S., Zhan, B., Jin, X., Talpin, J., Zhan, N.: Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. Theor. Comput. Sci. **903**, 1–25 (2022). https://doi.org/10.1016/J.TCS.2021.11.008

26. Yan, G., Jiao, L., Wang, S., Wang, L., Zhan, N.: Automatically generating SystemC code from HCSP formal models. ACM Trans. Softw. Eng. Methodol. **29**(1), 4:1–4:39 (2020). https://doi.org/10.1145/3360002

27. Zhan, B., Xu, X., Gao, Q., Ji, Z., Jin, X., Wang, S., Zhan, N.: Mars 2.0: A toolchain for modeling, analysis, verification and code generation of cyber-physical systems. CoRR abs/2403.03035 (2024). https://doi.org/10.48550/ARXIV.2403.03035

28. Zhao, J., Zhao, Y., Yao, P., Zeng, F., Zhan, B., Ren, K.: KBX: Verified model synchronization via formal bidirectional transformation. ACM Trans. Softw. Eng. Methodol. **34**(2) (2025). https://doi.org/10.1145/3696000