# A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements using TASTD ⋆

Alex Rodrigue Ndouna, Marc Frappier, Frédéric Mallet

► To cite this version:

Alex Rodrigue Ndouna, Marc Frappier, Frédéric Mallet. A Modular Orthogonal Integration of Opera-
tional and Prescriptive Timing Requirements using TASTD ⋆. SBMF 2025 - 28th Brazilian Symposium
on Formal Methods, Dec 2025, Recife, Brazil. 10.1007/978-3-032-12086-1_2. hal-05433530

HAL Id: hal-05433530

https://inria.hal.science/hal-05433530v1

Submitted on 28 Dec 2025

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 Attribution 4.0 International License
# A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements using TASTD*

Alex Rodrigue Ndouna¹,², Marc Frappier² and Frédéric Mallet³

¹ Université de Sherbrooke, Sherbrooke QC J1K 2R1, Canada
{Alex.Rodrigue.Ndouna,Marc.Frappier}@USherbrooke.ca

² Université Côte d'Azur, CNRS, Inria, I3S, Nice, France
Frederic.Mallet@univ-cotedazur.fr

**Abstract.** Designing and verifying safety-critical systems requires giving equal importance to non-functional and functional requirements from the start, especially those related to time. Since no single method can address all system aspects, a combination of formal methods is needed for accurate modeling and analysis. This paper proposes an integration of the CCSL (Clock constraints Specification language) and TASTD specification languages for the modular modeling of timing requirements. CCSL allows for the modular expression of timing constraints, whereas TASTD allows for the combination of state machines using CSP process algebra operators, to foster the construction of a system specification using the composition of small components specification. We propose rules to translate a CCSL specification into a TASTD specification, which can use the CSP [14] operators of TASTD to compose the CCSL constraints with other specification elements, like operating modes of a system. The CCSL part of the specification can be verified using CCSL tools. The global specification can be simulated using TASTD tools. The approach is demonstrated on a temperature control system which has been previously modeled using UML MARTE and CCSL, but for which no formal combination was available.

**Keywords:** TASTD, CCSL, formal method

## 1 Introduction

The formal design and verification of safety-critical systems requires capturing non-functional requirements with the same importance as functional requirements, right from the beginning. Among all, time plays a special role as many non-functional requirements directly depend upon it (e.g., energy, security). Time requirements include real-time constraints imposed by hardware or software components, but also timed or temporal functional requirements from the application itself. The literature provides plenty of rich models of time (e.g., Time(d) Automata [1], Petri nets [28], synchronous languages [6], timed process algebra [26], real-time scheduling [23]) that each come with ad-hoc efficient verification tools. To be efficient, each tool targets a decidable sub-class of problems but then demands to capture the requirements accordingly thus often altering the initial intents and very frequently omitting the functional part of the requirements as it falls outside the reach of the decidable sub-domain.

Real systems (whether industrial or not) have several characteristics, and most of the formal methods available today are either very general or focus on specific characteristics. No method can therefore simultaneously take into account all the different facets of a system to be developed or analyzed. Hence there is a need to use a combination of formal methods to model as faithfully as possible all aspects of a system before refinement and decomposition.

The Unified Modelling Language (UML) is one such method which intentionally attempts to provide a unified notation to capture all aspects of a system. So it has certain extensions, called profiles, which offer specialised notation for specific domains. The UML profile for MARTE is dedicated to modelling real-time and embedded systems. CCSL [2] has been designed as a formal companion language for MARTE to deal with time and causality in a very precise and concise way. The paper [27] shows two examples where a UML model is refined first with MARTE and second with CCSL to model two case studies. While CCSL comes with a formal semantics, the subset of UML/MARTE that was used does not give such guarantees. In this

<footnote>* Supported by Public Safety Canada's Cyber Security Cooperation Program (CSCP) and NSERC (Natural Sciences and Engineering Research Council of Canada).</footnote>
paper, we replace UML with TASTD [3], a strong, formal, state-based modeling language whose notation is syntactically close to UML State Machines, and which allows for the orthogonal combination of state machines using process algebra operators.

The contribution of this paper is as follows. We provide rules to translate CCSL operators into TASTD expressions and to combine them with other parts of a TASTD specification specifying other operational requirements like modes, to allow for a complete integration of CCSL within a TASTD specification. We prove the correctness of our translations to ensure that the translated expression have the same trace semantics as their corresponding CCSL expressions. The combination enables one to benefit from the advantages of each of the two languages, in particular the great expressiveness and modularity of the TASTD language and the verification tools offered by CCSL. The aspects modeled in CCSL can be verified using the tools offered by CCSL. We are currently developing several verification tools for TASTD, e.g., for proving local invariants in a TASTD specification [7] and a general meta-model framework for proving temporal properties [9], which will enable us to prove more properties on a CCSL-TASTD specification. This gives us a powerful heterogeneous formal modeling framework.

This paper is structured as follows. Section 2 presents an overview of the TASTD notation. Section 3 describes CCSL. Section 4 presents the translation rules from CCSL to TASTD and a proof of their correctness. Section 5 presents the CCSL and TASTD model of our case study, a temperature control system. Section 6 discusses the verification and validation of this model, while Section 7 concludes the paper.

# 2 TASTD

## 2.1 An Overview of TASTD

Timed Algebraic State-Transition Diagrams (TASTD) [3,4] is a time extension for ASTD [22]. TASTD allows for the composition of automata using CSP-like process algebra operators: sequence, choice, Kleene closure, guard, parameterized synchronization, flow (the AND states of Statecharts), and quantified versions of parameterized synchronization and choice. Each TASTD operator corresponds to a TASTD type. Elementary TASTDs are defined using automata. Automaton states can either be elementary or composite; a composite state can be of any TASTD type. Within a TASTD, a user can declare attributes (i.e., state variables). Actions written in C++ can be declared on automata transitions, states, and at the TASTD level; they are executed when a transition is triggered. These actions can modify TASTD attributes and execute arbitrary C++ code. Attributes can be of any C++ type.

TASTD introduces time-triggered transitions, i.e., transitions triggered when conditions referring to a global clock are satisfied. In ordinary ASTDs, only the reception of an event from the environment can trigger a transition. The special event *step* labels the timed-triggered transitions. *step* is treated as an event; its only particularity is that it is evaluated on a periodical basis. The specifier determines the value of the period according to the desired time granularity required to match system timing constraints. TASTD also introduces new timing operators that can perform *step* transitions: delay, persistent delay, timeout, persistent timeout, and timed interrupt. TASTDs rely on the availability of a global clock called *cst*, which stands for *current system time*. If the guard of a *step* transition is satisfied, the transition can be fired. TASTD is algebraic, in the sense that TASTD operators can be freely mixed as in a process algebra. The operational semantics of TASTD is formally defined in [4] using transition rules in the usual Plotkin style.

## 2.2 TASTD support tools

TASTD specifications can be edited with a graphical tool called eASTD [13] and translated into executable C++ programs using cASTD [13]. The generated C++ programs can be used as an actual implementation of the TASTD specification. cASTD can generate code for simulation, where a manual clock, which the specifier controls during the simulation, replaces the system clock. The specifier can decide to advance the clock to a specific time; the simulator generates the step events necessary to reach the specified time. Environment events can be submitted at these specified times. We use a simulation to validate the provided scenarios discussed in Section 6. Invariants can also be declared in TASTD expressions and automaton states. Proof obligations for invariant preservation are currently being developed and available for 4 ASTD types (automaton, guard, sequence and Kleene closure). A Rodin plugin to generate and discharge these proof obligations is currently under development [7].
# 3 The Clock Constraint Specification Language (CCSL)

## 3.1 An Overview of CCSL

In CCSL, logical clocks are used to model occurrences of events [29]. Each event that may occur in the system is represented by a clock that ticks when the corresponding event occurs. Constraints over clocks are used to specify causal and temporal relations between system events. Global physical time does not exist for the clocks and their constraints. A logical clock $c$ is defined by an infinite sequence $s_c(i)$ being tick or idle. The value of $s_c(i)$ indicates whether the associated event of $c$ occurs or not at step $i$. If $s_c(i)$ is tick, then the event occurs, otherwise not.

The semantics of CCSL of a CCSL operator is defined using traces called schedules. Given a set $C$ of clocks, a schedule of $C$ is a total function $\delta: \mathbb{N}^+ \to 2^C$ such that $\forall i \in \mathbb{N}^+, \delta(i) = \{c \in C | s_c(i) = \text{tick}\}$ and $\delta(i) \neq \emptyset$. A schedule defines a partial order between the ticks of the clocks. $\delta(i)$ is a subset of $C$ such that $c \in \delta(i)$ iff $c$ ticks at step $i$. For a given schedule $\delta$, the history function $\chi: C \times \mathbb{N}^+ \to \mathbb{N}$ returns the number of tick of a clock $c$ between steps 1 and $i-1$ in a schedule $\delta$. It is defined as follows:

$$ \chi(c, i) = \begin{cases} 0, & \text{if } i = 1; \\ \chi(c, i-1), & \text{if } i > 1 \land c \notin \delta(i-1); \\ \chi(c, i-1) + 1, & \text{if } i > 1 \land c \in \delta(i-1); \end{cases} $$

CCSL operators are defined in Table 1, where $b \ge 0$, $d \ge 0$, $p > 0$, $c_1, c_2, c_3$ are logical clocks and $w$ is a word over $\{0, 1\}$. An operational semantics of CCSL operators, by means of a clock-labeled transition system (LTS), has also been defined in [16]. The traces of a CCSL expression (constraint), defined in Table 1, are the same as the traces of its LTS.

The semantics of a set of CCSL constraints $S_1, \dots, S_n$ is their "conjunction", which is given by the synchronized product of $A_1 \times \dots \times A_n$, where each $A_i$ is the LTS representing $S_i$. Let $C_i$ be the clocks occurring in CCSL constraint $S_i$. A transition $(s_i, B, s'_i)$ in this LTS denotes that the set of clocks $B \subseteq C_i$ tick when transitioning from $s_i$ to $s'_i$. The translation of $S_i$ into $A_i$ is given in [18] and omitted here for the sake of concision. The LTS of the synchronized product $A_1 \times A_2$ is defined on the Cartesian product of the states of each LTS as follows:

$$ \begin{array}{l} ((s_1, s_2), B_1 \cup B_2, (s'_1, s'_2)) \\ \Leftrightarrow \\ (s_1, B_1, s'_1) \wedge (s_2, B_2, s'_2) \wedge B_1 \cap C_2 = B_2 \cap C_1 \end{array} \qquad (1) $$

CCSL constraints can be structured into 3 groups: synchronous constraints, asynchronous constraints and Synchronous constraints rely on the notion of coincidence of clock instants. For example, the subclock constraint $a \subseteq b$ specifies that each occurrence of $a$ (called the subclock) must coincide with exactly one occurrence of $b$ (called the superclock). Other examples of synchronous constraints are discretizedBy and exclusion (denoted $\#$). The latter prevents two clocks from ticking simultaneously. The former discretizes a dense clock to derive discrete chronometric clocks, mostly from IdealClk as the value for parameter $c_2$ of the operator, a perfect dense chronometric clock, predefined in the MARTE Time Library, and assumed to follow 'physical time' faithfully.

Asynchronous constraints are based on instant precedence, which may appear in a strict ($\prec$) or a non-strict ($\prec\prec$) form. The clock constraint $a \prec b$, also called fasterThan, specifies that clock $a$ is (non-strictly) faster than clock $b$, i.e., clock $b$ can produce its $k^{th}$ tick only if $a$ has produced at least $k$ ticks. The strict version ($\prec$) forbids the $k^{th}$ ticks of $a$ and $b$ to be synchronous, while the non-strict version ($\prec\prec$) allows it. The constraint $a \sim b$ or $a \prec_1 b$ states that $\forall k \in \mathbb{N}; a[k] \prec b[k] \land b[k] \prec a[k+1]$, i.e., an instant of $a$ precedes the instant of $b$ which in turn precedes the next instant of $a$. The conjunction $\land$ of two CCSL constraint is represented by the synchronised product of the LTS of these constraints.

Mixed constraints combine coincidence and precedence. The constraint $c = a \text{delayedFor } n$ on $b$ enforces a delayed coincidence, i.e., imposes $c$ to tick synchronously with the $n^{th}$ tick of $b$ following a tick of $a$. It is considered as a mixed constraint since $a$ and $b$ are not assumed to be synchronous.
<table><caption>Table 1: Semantics of CCSL with respect to schedules</caption><thead><tr><th>CCSL operator</th><th>Condition for a valid trace</th></tr></thead><tbody><tr><td>Precedence (c<sub>1</sub>[b] &lt; c<sub>2</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.χ(c<sub>2</sub>, n) - χ(c<sub>1</sub>, n) = b ⇒ c<sub>2</sub> &notin; δ(n)</td></tr><tr><td>c<sub>1</sub> &lt; c<sub>2</sub></td><td>c<sub>1</sub>[0] &lt; c<sub>2</sub></td></tr><tr><td>c<sub>1</sub> &lt;_b c<sub>2</sub></td><td>c<sub>1</sub> &lt; c<sub>2</sub> &and; c<sub>2</sub>[b] &lt; c<sub>1</sub></td></tr><tr><td>Causality (c<sub>1</sub> &le; c<sub>2</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.χ(c<sub>1</sub>, n) &ge; χ(c<sub>2</sub>, n)</td></tr><tr><td>Subclock (c<sub>1</sub> &subseteq; c<sub>2</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.c<sub>1</sub> ∈ δ(n) ⇒ c<sub>2</sub> ∈ δ(n)</td></tr><tr><td>Exclusion (c<sub>1</sub> # c<sub>2</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.c<sub>1</sub> &notin; δ(n) &or; c<sub>2</sub> &notin; δ(n)</td></tr><tr><td>Union (c<sub>1</sub> &triangleq; c<sub>2</sub> + c<sub>3</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.c<sub>1</sub> ∈ δ(n) ⇔ c<sub>2</sub> ∈ δ(n) &or; c<sub>3</sub> ∈ δ(n)</td></tr><tr><td>Intersection (c<sub>1</sub> &triangleq; c<sub>2</sub> * c<sub>3</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.c<sub>1</sub> ∈ δ(n) ⇔ c<sub>2</sub> ∈ δ(n) &and; c<sub>3</sub> ∈ δ(n)</td></tr><tr><td>Infimum (c<sub>1</sub> &triangleq; c<sub>2</sub> &and; c<sub>3</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.χ(c<sub>1</sub>, n) = max(χ(c<sub>2</sub>, n), χ(c<sub>3</sub>, n))</td></tr><tr><td>Supremum (c<sub>1</sub> &triangleq; c<sub>2</sub> &or; c<sub>3</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.χ(c<sub>1</sub>, n) = min(χ(c<sub>2</sub>, n), χ(c<sub>3</sub>, n))</td></tr><tr><td>Periodicity (c<sub>1</sub> &triangleq; c<sub>2</sub> &alpha; p)</td><td>∀n ∈ &#x2126;<sup>+</sup>.c<sub>1</sub> ∈ δ(n) ⇔ (c<sub>2</sub> ∈ δ(n) &and; &exist;m ∈ &#x2126;<sup>+</sup>.χ(c<sub>2</sub>, n) = m &times; p - 1)</td></tr><tr><td>Filtering (c<sub>1</sub> &triangleq; c<sub>2</sub> &darr; w)</td><td>∀n ∈ &#x2126;<sup>+</sup>.c<sub>1</sub> ∈ δ(n) ⇔ (c<sub>2</sub> ∈ δ(n) &and; w[χ(c<sub>2</sub>, n)mod|w|])</td></tr><tr><td>DelayFor (c<sub>1</sub> &triangleq; c<sub>2</sub>$d on c<sub>3</sub>)</td><td>∀n ∈ &#x2126;<sup>+</sup>.c<sub>1</sub> ∈ δ(n) ⇔ (c<sub>3</sub> ∈ δ(n) &and; &exist;m ∈ &#x2126;<sup>+</sup>.(c<sub>2</sub> ∈ δ(m) &and; χ(c<sub>3</sub>, n) - χ(c<sub>3</sub>, m) = d))</td></tr><tr><td>discretizedBy (c<sub>1</sub> &triangleq; c<sub>2</sub> discretizedBy d)</td><td>∀n ∈ &#x2126;<sup>+</sup>.c<sub>1</sub> ∈ δ(n) ⇒ c<sub>2</sub> ∈ δ(n) where c<sub>2</sub> ticks every d units of time</td></tr><tr><td>alternatesWith (c<sub>1</sub> &sim; c<sub>2</sub>)</td><td>c<sub>1</sub> &lt; c<sub>2</sub> &and; c<sub>2</sub>[1] &lt; c<sub>1</sub></td></tr></tbody></table>

## 3.2 CCSL support tools

CCSL was introduced as part of UML MARTE by OMG in 2011. The main tool to handle CCSL and conduct verification is TimeSquare [12] 3 4. TimeSquare can produce simulations for a given CCSL specification but also decide whether no schedule is possible. It can build both explicit (when finite) and symbolic representations of the possible schedules. If no schedule is possible, there is a flaw in the specification. Usually there is an unbounded number of possible schedules, in which case the tool looks for schedules that can be implemented with finite memory (called safe schedules). When it is safe, the tool exports a representation that can be used to conduct LTL model-checking. Output formats available include NuXMV [8], UPPAAL [5], Z3 [20], Kieler [25], which are third-party tools that are largely used by the community. Specific experiments to exploit SMT tools like Z3 in an efficient way have been conducted on a separate tool called MyCCSL [10] 5.

# 4 Translating CCSL operators in TASTD

## 4.1 General concepts used in translation

Before proposing our different translations of CCSL operators in TASTD, we first describe how the basic concepts of CCSL in TASTD are modeled.

Given a system with *n* logical clocks, we use an ASTD event called Schedule(?clock) that takes a vector clock ∈ 0..(*n*−1) → bool as an input parameter (decoration “?”) to receive clock values. We have clock[*i*−1] = 1 when the *i*th clock has ticked in that step.

One might be tempted to trivially model CCSL’s notion of history χ by an array of integers of size *n*, called history, which would keep track of the number of ticks of each clock. The history array would be unique and global for the entire specification. In accordance with CCSL’s definition of history, each element of the history would be initialized to 0. Taking advantage of TASTD’s ability to inject utility functions implemented in C++ into our specification, we would have an updateHistory/history/clock function that will be called at each step to update history using clock. But using a history array to save history could lead to memory overflow. To avoid memory overflow, each CCSL constraint is translated into an ASTD, each ASTD contains local variables to store the necessary information, implemented by counters, to represent the

<footnote n="3">3 https://timesquare.inria.fr</footnote>

<footnote n="4">4 https://github.com/frederic-mallet/ccsl-sts.</footnote>

<footnote n="5">5 http://re4cps.org/download.</footnote>
CCSL constraint. These ASTDs are then composed using synchronization to represent the conjunction of
these constraints.

In [17,19] it is shown how to prove that a CCSL constraint can be implemented using bounded memory. This approach transforms a specification of a CCSL operator into A directed marked graph [11] where it is easier to demonstrate memory bounding. Based on this work, we optimize our translation by using local counters in the ASTD representing a CCSL constraint that refers to history in its semantics. The counters associated with the CCSL operators are updated at each transition execution in the system. To update the counters we will define three functions. Function `clockCounterDiff` (*counter*, *c*₁, *c*₂, *clock*) which takes the counter, two clocks and the clock array as parameters and updates the counter by performing the action *counter* := *counter* + *clock*[*c*₁] - *clock*[*c*₂]. This function will be used to update the counters for the operators *Precedence*, *Causality*, *Infimum* and *Supremum*. We have the function `clockCounterMod`(*counter*, *c*₁, *clock*, *p*) which updates the counter by applying the action *counter* := (*counter* + *clock*[*c*₁])%*p*. This function will be used to update the counters for the operators *Periodicity* and *Filtering* with *p* = *w*.size().

## 4.2 Translation

The translation of a CCSL specification consisting of a set of constraints $A = \{S_1, \dots, S_n\}$ is given by a synchronization TASTD $T(S) = T(S_1) \parallel \dots \parallel T(S_n)$, where $T(S_i)$ is a TASTD automaton representing the CCSL constraint $S_i$. TASTD's synchronization operator `||` is CSP's parallel operator `||`. It represents the conjunction of the CCSL constraints. Figure 1 illustrates the structure of $T(S)$. For the translation of a CCSL

<figure><img src="image_2.png" /><figcaption>Fig. 1: The TASTD $T(S)$ represent a CCSL specification</figcaption></figure>

$$S = \{S_1, \dots, S_N\}$$

constraint into an automaton TASTD, we use the template automaton TASTD shown in Figure 2, which simply consists of a state $s_0$ with a single reflexive transition `Schedule钟 clock)`. The guard and the action of the transition depend on the CCSL operator to translate. Table 2 shows, for each of the CCSL operators, the guard of the transition, written using the C++ syntax. One can see that the translation is directly derived from Table 1. For example, for precedence ($c_1 [b] \prec c_2$), the difference $\chi(c_2, n) - \chi(c_1, n)$ will be implemented by using a counter variable which, for each tick, will keep track of the difference between the number of times $c_2$ and $c_1$ appear in the system. The semantics of CCSL for accepting a clock tick at step $n$ only refers to $\chi(\dots, n)$. Condition $c \in \delta(n)$ is represented by `clock[c] == 1`, i.e., the value of the clock $c$ in parameter `clock`.

<figure><img src="image_3.png" /><figcaption>Fig. 2: TASTD representing a CCSL constraint</figcaption></figure>

For the translation of *DelayFor* (*c*₁ ≜ *c*₂*d* on *c*₃) operator, we use an array of size *d* of Boolean initialised at 0 called *Buffer*. This array will allow us to keep track of the appearance of the clocks affected by the operator. *Buffer* works like a right-shift register and to update it we use the function *updateBuffer*(*c*₂, *c*₃, *clock*, *Buffer*, *d*) which, when clock *c*₂ ticks, sets a value of 1 in the first position of *Buffer*, and if *c*₃ ticks, all the values in *Buffer* are shifted to the right by resetting the first position of *Buffer* to 0. In this way, a tick from *c*₁ can only be obtained when *c*₃ also has a tick and *Buffer*[*d* − 1] == 1, *Buffer*.
<table><caption>Table 2: Transition guard of event Schedule(*clock*) for each CCSL operator, expressed in C++</caption><thead><tr><th>Operators (Parameters)</th><th>guard</th></tr></thead><tbody><tr><td>Precedence (c<sub>1</sub>[b] &lt; c<sub>2</sub>)</td><td>(counter != b) || (clock[c<sub>2</sub>] == 0)</td></tr><tr><td>Causality (c<sub>1</sub> &lt;= c<sub>2</sub>)</td><td>(counter + clock[c<sub>1</sub>] - clock[c<sub>2</sub>]) &gt;= 0</td></tr><tr><td>Subclock (c<sub>1</sub> &subseteq; c<sub>2</sub>)</td><td>((clock[c<sub>1</sub>] == 0) || (clock[c<sub>2</sub>] == 1))</td></tr><tr><td>Exclusion (c<sub>1</sub> &ne; c<sub>2</sub>)</td><td>((clock[c<sub>1</sub>] == 0) || (clock[c<sub>2</sub>] == 0))</td></tr><tr><td>Union (c<sub>1</sub> &triangle; c<sub>2</sub> + c<sub>3</sub>)</td><td>(clock[c<sub>1</sub>] == (clock[c<sub>2</sub>] || clock[c<sub>3</sub>]))</td></tr><tr><td>Intersection (c<sub>1</sub> &triangle; c<sub>2</sub> * c<sub>3</sub>)</td><td>(clock[c<sub>1</sub>] == (clock[c<sub>2</sub>] &amp;&amp; clock[c<sub>3</sub>]))</td></tr><tr><td>Infimum (c<sub>1</sub> &triangle; c<sub>2</sub> &amp; c<sub>3</sub>)</td><td>(counter == 0)?(clock[c<sub>1</sub>] == (clock[c<sub>2</sub>] || clock[c<sub>3</sub>])) : (counter > 0)?<br>clock[c<sub>1</sub>] == clock[c<sub>2</sub>] : clock[c<sub>1</sub>] == clock[c<sub>3</sub>]</td></tr><tr><td>Supremum (c<sub>1</sub> &triangle; c<sub>2</sub> &amp; c<sub>3</sub>)</td><td>(counter == 0)?(clock[c<sub>1</sub>] == (clock[c<sub>2</sub>] || clock[c<sub>3</sub>])) : (counter < 0)?<br>clock[c<sub>1</sub>] == clock[c<sub>2</sub>] : clock[c<sub>1</sub>] == clock[c<sub>3</sub>]</td></tr><tr><td>Periodicity (c<sub>1</sub> &triangle; c<sub>2</sub> &ne; p)</td><td>(clock[c<sub>1</sub>] == clock[c<sub>2</sub>]) &amp;&amp; (counter == 0)</td></tr><tr><td>Filtering (c<sub>1</sub> &triangle; c<sub>2</sub> &ne; w)</td><td>clock[c<sub>1</sub>] == (clock[c<sub>2</sub>] &amp;&amp; (w(counter] == 1))</td></tr><tr><td>DelayFor (c<sub>1</sub> &triangle; c<sub>2</sub>$d on c<sub>3</sub>)</td><td>(clock[c<sub>1</sub>] == clock[c<sub>3</sub>]) &amp;&amp; (Buffer[d &minus; 1] == 1)</td></tr><tr><td>discretizedBy (p = IdealClk<br>discretizedBy d)</td><td>!(clock[p] == 1) || ideal_clock-expired(d)</td></tr></tbody></table>

To translate the *discretizedBy* operator, we need to implement the notion of *idealClock* in ASTD, and to do this we use its ASTD equivalent, the *Timer* object. A *Timer* in ASTD is a C++ class with a timestamp attribute of type *std::time_t*, which defaults to the current time when instantiated, and has functions such as *expired(double duration)*, which determines whether a duration (in nanoseconds) has elapsed between the timestamp value and the current time, and the object has a *reset_clock()* function, which resets the timestamp to the current time. The *discretizedBy* operator is therefore translated by declaring a local variable *ideal_clock* of type *Timer*, which only accepts the transition when *ideal_clock.expired(d)* is true, and after the transition has been executed, the *ideal_clock.reset_clock()* action is called to reset our clock for the next iteration of the periodicity.

Table 3 shows the logic for updating the counters associated with each operator. Depending on the operator, the transition will execute either *updateBuffer*, *clockCounterMod* or *clockCounterDiff*.

<table><caption>Table 3: Counter update logic for each type of operator</caption><thead><tr><th>Operators</th><th>Counter update action</th></tr></thead><tbody><tr><td>Precedence (c<sub>1</sub> [b] &lt; c<sub>2</sub>)</td><td>clockCounterDiff(counter, c<sub>2</sub>, c<sub>1</sub>, clock)</td></tr><tr><td>Causality (c<sub>1</sub> &lt;= c<sub>2</sub>)</td><td>clockCounterDiff(counter, c<sub>1</sub>, c<sub>2</sub>, clock)</td></tr><tr><td>Infimum (c<sub>1</sub> &triangle; c<sub>2</sub> &amp; c<sub>3</sub>)</td><td>clockCounterDiff(counter, c<sub>2</sub>, c<sub>3</sub>, clock)</td></tr><tr><td>Supremum (c<sub>1</sub> &triangle; c<sub>2</sub> &amp; c<sub>3</sub>)</td><td>clockCounterDiff(counter, c<sub>2</sub>, c<sub>3</sub>, clock)</td></tr><tr><td>Periodicity (c<sub>1</sub> &triangle; c<sub>2</sub> &ne; p)</td><td>clockCounterMod(counter, c<sub>1</sub>, clock, p)</td></tr><tr><td>Filtering (c<sub>1</sub> &triangle; c<sub>2</sub> &ne; w)</td><td>clockCounterMod(counter, c<sub>2</sub>, clock, w.size())</td></tr><tr><td>DelayFor (c<sub>1</sub> &triangle; c<sub>2</sub>$d on c<sub>3</sub>)</td><td>updateBuffer(c<sub>2</sub>, c<sub>3</sub>, clock, Buffer, d)</td></tr></tbody></table>

<figure><img src="image_4.png" /><figcaption>Fig. 3: Complete translation of a precedence constraint</figcaption></figure>
Figure 3 shows an example of an ASTD automaton obtained at the end of the complete translation of a CCSL constraint, in this case the complete translation of the precedence constraint.

## 4.3 Correctness of the Translation

Since the translation of each CCSL operator into an automaton TASTD is straightforward, it remains to show that the synchronized product of CCSL constraints is equivalent to the synchronization operator of TASTD, which is defined as CSP's parallel product. Given CCSL specifications $S_1, \dots, S_n$, and their corresponding LTS $A_1, \dots, A_n$, we must prove that $A_1 \times \dots \times A_n$ is trace-equivalent to $T(S_1) \parallel \dots \parallel T(S_n)$.

In TASTD, $T(S_i)$ is represented by a TASTD automata with a single transition of the form $[G_i]e(\?B)$, where the guard $G_i$ refers only to clocks of $C_i$ and $B$ is the set of all clocks occuring in $S$ (i.e., $B = \cup_i C_i$). Since the evaluation of the guard $G_i$ depends only on the clock of $C_i$, we have that $G(B) \Leftrightarrow G(B \cap C_i)$. We have already argued that $T(S_i)$ and $S_i$ are trace equivalent by construction. This means that for any trace accepted by both, each transition $(s_i, B, s'_i)$ in a run of $A_i$ is matched by a transition $Q_i \xrightarrow{B} Q'_i$ in $T(A_i)$, and vice-versa. To prove the equivalence between the synchronized product of two CCSL constraints and parallel synchronization in TASTD, we establish Theorem 1 that we will demonstrate next.

**Theorem 1.** Let $A_1, A_2$ be two LTS that represent two CCSL constraints. Then $A_1 \times A_2$ and $T(A_1) \parallel T(A_2)$ are trace equivalent.

To demonstrate this, we are going to prove that a transition in a run of $A_1 \times A_2$ is matched by a transition in a run of $T(A_1) \parallel T(A_2)$ and vice-versa. For the sake of concision, we denote $(s_i, B, s'_i) \in A_i$ by simply writing $(s_i, B, s'_i)$, and we denote a transition in $T(S_i)$ by $Q_i \xrightarrow{B} Q'_i$. The equivalence to be demonstrated is as follows.

$$((s_1, s_2), B_1 \cup B_2, (s'_1, s'_2)) \Leftrightarrow (Q_1, Q_2) \xrightarrow{e(B)} (Q'_1, Q'_2)$$

with $B = B_1 \cup B_2$.

– Proof of direction $\Rightarrow$

$$
\begin{array}{l@{\hspace{2em}}r@{\quad}l}
((s_1, s2), B, (s'_1, s2')) & \langle \text{definition of } \times (1) \rangle & \\
\Leftrightarrow & & \\
(s_1, B_1, s'_1) \land (s_2, B_2, s'_2) \land B_1 \cap C_2 = B_2 \cap C_1 & \langle \text{Trace equivalence of } A_i \text{ and } T(S_i) \rangle & \\
\Leftrightarrow & & \\
Q_1 \xrightarrow{e(B_1)} Q'_1 \land Q_2 \xrightarrow{e(B_2)} Q'_2 \land B_1 \cap C_2 = B_2 \cap C_1 & \langle \text{lemma 1 (see below)} \rangle & \\
\Leftrightarrow & & \\
Q_1 \xrightarrow{e(B \cap C_1)} Q'_1 \land Q_2 \xrightarrow{e(B \cap C_2)} Q'_2 & \langle G(B) \Leftrightarrow G(B \cap C_i) \rangle & \\
\Leftrightarrow & & \\
Q_1 \xrightarrow{e(B)} Q'_1 \land Q_2 \xrightarrow{e(B)} Q'_2 & \langle \text{semantics of } \parallel \text{ in TASTD} \rangle & \\
\Leftrightarrow & & \\
(Q_1, Q_2) \xrightarrow{e(B)} (Q'_1, Q'_2) & &
\end{array}
$$

– Proof of direction $\Leftarrow$

$$
\begin{array}{l@{\hspace{2em}}r@{\quad}l}
(Q_1, Q_2) \xrightarrow{e(B)} (Q'_1, Q'_2) & \langle \text{def. of } \parallel \rangle & \\
\Leftrightarrow & & \\
Q_1 \xrightarrow{e(B)} Q'_1 \land Q_2 \xrightarrow{e(B)} Q'_2 & \langle G(B) \Leftrightarrow G(B \cap C_i) \rangle & \\
\Leftrightarrow & & \\
Q_1 \xrightarrow{e(B \cap C_1)} Q'_1 \land Q_2 \xrightarrow{e(B \cap C_2)} Q'_2 & \langle \text{Trace equivalence of } A_i \text{ and } T(S_i) \rangle & \\
\Leftrightarrow & & \\
(S_1, B \cap C_1, S'_1) \land (S_2, B \cap C_2, S'_2) & \langle \text{identity } B \cap C_1 \cap C_2 = B \cap C_2 \cap C_1 \rangle & \\
\Leftrightarrow & & \\
(S_1, B \cap C_1, S'_1) \land (S_2, B \cap C_2, S'_2) \land (B \cap C_1) \cap C_2 = (B \cap C_2) \cap C_1 & \langle \text{definition of } \times (1) \rangle & \\
\Leftrightarrow & &
\end{array}
$$
$$ ((S_1, S_2), (B \cap C_1) \cup (B \cap C_2), (s'_1, s'_2)) \in T \qquad \langle \text{set theory} \rangle $$

$$ ((S_1, S_2), B \cap (C_1 \cup C_2), (s'_1, s'_2)) \in T \qquad \langle C = C_1 \cup C_2 \rangle $$

$$ ((S_1, S_2), B \cap C, (s'_1, s'_2)) \in T \qquad \langle B \subseteq C \rangle $$

$$ ((S_1, S_2), B, (s'_1, s'_2)) \in T \qquad \langle B = B_1 \cup B_2 \rangle $$

$$ ((S_1, S_2), B_1 \cup B_2, (s'_1, s'_2)) \in T \qquad \langle \square \rangle $$

**Lemma 1.** ($B_1 \cap C_2 = B_2 \cap C_1$) $\Rightarrow$ $B \cap C_1 = B_1 \wedge B \cap C_2 = B_2$

We only show $B \cap C_1 = B_1$; the proof of $B \cap C_2 = B_2$ is similar.

$$ B \cap C_1 = (B_1 \cup B_2) \cap C_1 \qquad \langle \text{Def. of } B \rangle $$

$$ = (B_1 \cap C_1) \cup (B_2 \cap C_1) \qquad \langle \text{distributivity} \rangle $$

$$ = B_1 \cup (B_2 \cap C_1) \qquad \langle B_1 \subseteq C_1 \rangle $$

$$ = B_1 \cup (B_1 \cap C_2) \qquad \langle B_1 \cap C_2 = B_2 \cap C_1 \rangle $$

$$ = B_1 \qquad \langle B_1 \cap C_2 \subseteq B_1 \rangle \qquad \square $$

# 5 Case Study: Temperature Control System (TCS)

We consider a simplified version of a temperature control system [27] that regulates the temperature inside a nuclear reactor core, by using thermal-controlling rods. The rods are inserted into the core of the reactor when the temperature reaches a given upper limit, denoted by constant MAX, causing the temperature to gradually reduce (as neutrons in the reactor are absorbed by the control rods). Similarly, the control rods are removed when the temperature in the reactor falls below MIN. TCS operates in two modes, Diagnostic and Control.

In Diagnostic mode, the following actions are triggered that execute the corresponding behaviors: Diagnostics examines the current status of the control rods, Reconfig replaces the ineffective control rods if any, and StatusUpdate updates the status of a rod configuration in the reactor. In Control mode, the system triggers three actions; PeriodicSense senses the temperature in the reactor, InsertRod inserts a control rod, and RemoveRod removes a rod from the reactor.

After 100 s in Diagnostic mode, the system changes to Control mode. However, the mode change from Control to Diagnostic is triggered by an event occurring when the sensed temperature in the reactor is within the specified limits. The following properties specify the functional and timing aspects for TCS:

* TCS1 : Diagnostics is always followed by Reconfig.

* TCS2 : The behavior of Reconfig is 'extended' by StatusUpdate, only when there is a change in the control rod configuration.

* TCS3 : PeriodicSense executes periodically with a period of 10s.

* TCS4 : PeriodicSense is followed by InsertRod or RemoveRod but not both.

* TCS5 : At most two rods can be used in sequence, for cooling the reactor core.

The correspondence between the actions and the logical clocks in the CCSL constraints is as follows: Diagnostics : d, Reconfig : c, StatusUpdate : s, PeriodicSense : p, InsertRod : i, and RemoveRod : r. The functional and timing properties of the TCS, as CCSL constraints, are: TCS1 : d ~ c, TCS2 : s ~ c, TCS3 : Clock p = IdealClk discretizedBy 10s, TCS4 : p ~ (i \cup r) \wedge i \neq r, TCS5 : i \prec_2 r.

We translate the CCSL constraints using the translation described in the previous section, and we combine the resulting TASTDs using the TASTD synchronization operator. The TCS1 constraint can be translated into a CCSL base constraint as follows: $d \prec c \wedge c$ [1] $\prec$ d. The basic CCSL constraints refer to the CCSL
constraints listed in the table 1. Following the same logic, we decompose the TCS4 constraint into the product of basic operators and we have: $p \prec z \wedge z$ [1] $\prec p \wedge z = i \cup r \wedge i \# r$.

All the basic CCSL constraints to be translated into TASTD for our study, after decomposing all our initial constraints into products of basic CCSL operators are: $TCS1_1: d \prec c$, $TCS1_2: c$ [1] $\prec d$, $TCS2: s \subseteq c$, $TCS3: \mathbf{Clock} p = \mathbf{IdealClk discretizedBy}$ 10 $s$, $TCS4_1: p \prec z$, $TCS4_2: z$ [1] $\prec p$, $TCS4_3: z = i \cup r$, $TCS4_4: i \# r$, $TCS5: i \prec_2 r$

<figure><img src="image_5.png" /><figcaption>Fig. 4: The TASTD specification of the TCS case study</figcaption></figure>

Our case study has 2 operating modes: *Diagnostic*, which is responsible for implementing the constraints *TCS1.1*, *TCS1.2*, *TCS2*, and *Control*, which implements constraints *TCS3*, *TCS4.1*, *TCS4.2*, *TCS4.3*, *TCS4.4*, *TCS5*. Each constraint is implemented according to the generic TASTD model shown in Figure 2 and, depending on the type of operator to be translated, the guard and actions is defined as shown in Table 2.

Figure 4 (c) shows the TASTD for the behaviour of the *Diagnostic* mode. It is a synchronization of *TCS1.1*, *TCS1.2* and *TCS2*. Mode *Control* is carried out using a synchronization of *TCS4.1*, *TCS4.2*, *TCS4.3*, *TCS4.4*, *TCS5*. Figure 4 (b) shows the general structure TASTD control, synchronising the constraints relating to this mode. Switching from *Diagnostic* mode to *Control* mode is done automatically after running the *Diagnostic* mode for 100 *s*. To model it in TASTD we first initialise a timeout variable to 0, in this case the *diagnostic_to_control* variable. This variable counts the time spent in the mode. To switch from *Diagnostic* mode to *Control* mode we use a *step* transition, which is a transition that is periodically automatically triggered in a TASTD, following the system clock. We associate a guard with the *step* transition so that it is only executed when the variable accounting for the time spent in *Diagnostic* mode has a value greater than or equal to 100 *s*. So, after 100 *s* spent in *Diagnostic* mode, the *step* transition is triggered and *Control* mode is launched. The basic unit of time being the nanosecond in TASTD, in the implementation we check instead that $1E+11$ nanoseconds have elapsed, corresponding to 100 *s*, which explains the appearance of the value $1E11$ in Figure 4 (a).

On the other hand, to switch from mode *Control* to mode *Diagnostic*, the reactor temperature must be between a minimum and a maximum temperature, called *MIN* and *MAX* respectively in our model. To model this transition from *Control* to *Diagnostic*, we use a *backToDiagnostic* transition between the two modes, which take an integer *temp* parameter as input, representing the current reactor temperature, and use its guard to check whether the temperature taken as input meets the *MIN* < *temp* < *MAX* constraint. If the constraint is met, we go into *Diagnostic* mode, otherwise we continue in *Control* mode. Figure 4 (a) shows the TCS TASTD modelling our case study, focusing only on communication between the two modes.

The TCS TASTD takes 9 variables as parameters: *MAX* and *MIN* corresponding respectively to the maximum and minimum values of the reactor temperature, then we have *d*, *c*, *s*, *p*, *i*, *r* and *z* which correspond respectively to the indices of the *Diagnostics*, *Reconfig*, *StatusUpdate*, *PeriodicSense*, *InsertRod* and *RemoveRod* events in the binary sequence of clock ticks. The *z* parameter corresponds to a clock which
ticks when one of the *InsertRod* or *RemoveRod* event occurs; it has been added to take into account of the *TCS4.3* basic constraint.

# 6 Validation and Verification

One of the advantages of TASTD is the ability to generate C++ code ready for compilation and execution to test the modelling of the problem to be solved. The ability to translate a CCSL specification into a TASTD therefore extends CCSL by providing an environment for testing specifications in simulation mode. Since CCSL is an extension of MARTE, which is itself a UML profile for specifying real-time systems, with this translation of CCSL into TASTD we can have a problem specification path going from UML to the generation of executable C++ code that can be tested in simulation mode to ensure the accuracy of our modelling.

To validate our model, we use an interactive animation of the specification with the executable code generated by the cASTD compiler for the simulation. Compilation is automatic and no human modification is required after code generation. We execute the compiled code and compare the results obtained with the requirements demanded by the case study to ensure that all the constraints are met each time an event is executed. However, execution of the compiled code and comparison with the trace provided is manual. We implemented four test cases to test our specification: one test case to simulate the execution of actions in *Diagnostic* mode, one test case to simulate the execution of *Diagnostic* mode then switch to *Control* mode after 100 s, one test case to test the execution of actions in *Diagnostic* mode followed by a switch to *Control* mode after 100 s and execution of actions in *Control* mode, one test case to test execution of *Diagnostic* mode followed by a switch to *Control* mode and a return to execution of *Diagnostic* mode after a change in system temperature. Our TASTD specification for the TCS study case is available here [21], with the executable source code for our specification and the various test cases presented for validating and verifying our specification.

Prior to this work, TASTD had no tools for verifying certain properties such as LTL and safety properties. One of the relevant aspects of this work is to enable this translation to fill this gap in TASTD by equipping it with certain tools enabling the verification of certain safety properties thanks to CCSL. CCSL would enable certain properties to be verified before translation, and which would then be kept true by the translation so that they would always remain verified on the TASTD specification resulting from the translation, whether in a complete modeling logic in TASTD or in a heterogeneous modeling system in both TASTD and CCSL. The first verifiable safety property is the bounding of the counters used to track the history. We perform a counter bounding check to ensure that there is no capacity or memory overflow for local counters. Here we ensure that, for translation purposes, the counters are finite, but this only depends on the use of these operators or the modeling of the specification, as we may come across cases where the counter cannot be bounded according to the modeling. We can translate all CCSL specifications into TASTD, whether they are partial or not, and then use CCSL to say whether it's safe or not, and saying it's safe means that all counters are bounded. If not all counters are bounded, this implies potential undesirable behavior during simulation due to a potential memory overflow of one of the unbounded counters.

Other properties that can be checked using CCSL include the consistency of the specification, because requirements are usually translated into CCSL from English, and English is often ambiguous, which means that problem specifications are not written in a consistent way. So CCSL allows us to know and check whether the problem posed has a potential solution before translation into TASTD, which is possible but very complex to do directly with TASTDs. But the absence of a solution to a problem can also be caused by deadlocks, which can be partial or local, or even called a bad path in CCSL, referring to an often infinite execution of the program without reaching an acceptance state. With CCSL, we can also detect these deadlocks beforehand.

Figure 5 shows the CCSL specification for our case study. Using the tool LightCCSL [15], we can generate its LTS, which helps to visualise all possible states and transitions according to the specified constraints, thus ensuring that the behaviour of the system respects the defined temporal and logical requirements.

Another important advantage of our translation is the possibility of using it to set up an observer system to validate the actions taken by an ASTD specification which was independently and manually derived. As TASTD is a more expressive language than CCSL, this means that in certain cases, it is more efficient to implement the system using a manually derived ASTD, rather than using the ASTD obtained from the CCSL to ASTD translation. But in this case, the ASTD obtained by translation remains important, as it will enable us to carry out the necessary checks on safety properties. The ASTD obtained by translation will be coupled
<figure><img src="image_6.png" /><figcaption>Fig. 5: CCSL case specification</figcaption></figure>

with the manually derived ASTD. An event is submitted to both. It must accepted/rejected by both ASTDs to be valid. The ASTD obtained by translation is called an *Observer*. This ensures that the manually derived ASTD satisfies safety properties that have been checked on the CCSL specification of the observer.

# 7 Conclusion

We have presented the methodology for translating CCSL operators into TASTD. For each CCSL operator, we define rules to construct an equivalent TASTD, which generally consists of an automaton TASTD with a state that has a reflexive transition and whose guard and actions depend on the operator being translated. We then proved that the product of CCSL operators is equivalent to the synchronization of TASTD, which allows us to translate a CCSL system specification into an equivalent TASTD system specification.

We tested our approach for translating CCSL into TASTD by applying it to the TCS system case study. We then validated and verified the translation using several test cases. The work presented here is a solid the basis to integrate TASTD and CCSL together to specify critical systems and thus take advantage of the benefits of both languages. Certain parts of the system shall be specified in CCSL and others in TASTD, like transfer between operating modes, which cannot be done in CCSL. We shall then be able to check certain important properties of the system on the parts specified in CCSL by taking advantage of the model checkers associated with CCSL.

The next stage of our work is therefore to determine how global properties of a TASTD specification can be proved from local properties checked using TASTD or CCSL verification mechanisms. This allows for modular verification, which should hopefully streamline the proving of global properties on large systems, using its TASTD decomposition. Event-B theories will be used to construct and verify the derivation of global properties from local properties, following the approach described in [24]. A theory of a TASTD meta-model has been recently developed [9]; we also plan to develop one for CCSL.
References

1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. **126**(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8

2. André, C.: Syntax and Semantics of the Clock Constraint Specification Language (CCSL). Research Report RR-6925, INRIA (2009), https://inria.hal.science/inria-00384077

3. de Azevedo Oliveira, D., Frappier, M.: TASTD: A real-time extension for ASTD. In: Glässer, U., Campos, J.C., Méry, D., Palanque, P.A. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 142–159. Springer (2023). https://doi.org/10.1007/978-3-031-33163-3_11

4. de Azevedo Oliveira, D., Frappier, M.: Technical Report 27 - Extending ASTD with real-time. https://github.com/DiegoOliveiraUDES/astd-tech-report-27 (2023)

5. Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exp. **41**(2), 133–142 (2011). https://doi.org/10.1002/SPE.1006

6. Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages 12 years later. Proceedings of the IEEE **91**(1), 64–83 (2003)

7. Cartellier, Q., Frappier, M., Mammar, A.: Proving local invariants in ASTDs. In: Li, Y., Tahar, S. (eds.) ICFEM 2023. Lecture Notes in Computer Science, vol. 14308, pp. 228–246. Springer (2023). https://doi.org/10.1007/978-981-99-7584-6_14

8. Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuxmv symbolic model checker. In: CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_22

9. Chen, C., Rivière, P., Singh, N.K., Dupont, G., Ait Ameur, Y., Frappier, M.: A proof-based ground algebraic meta-model for reasoning on astd in event-b. In: O’Conner, L. (ed.) IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE) (2025)

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

11. Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs. J. Comput. Syst. Sci. **5**(5), 511–523 (Oct 1971)

12. Deantoni, J., Mallet, F.: Timesquare: Treat your models with logical time. In: TOOLS (50). Lecture Notes in Computer Science, vol. 7304, pp. 34–41. Springer (2012). https://doi.org/10.1007/978-3-642-30561-0_4

13. Frappier, M.: ASTD support tools repo. https://github.com/DiegoOliveiraUDES/ASTD-tools (2023)

14. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)

15. Mallet, F.: LightCCSL tools repo. https://github.com/frederic-mallet/ccsl-sts

16. Mallet, F.: Automatic generation of observers from MARTE/CCSL. In: RSP 2012. pp. 86–92. IEEE (2012). https://doi.org/10.1109/RSP.2012.6380695

17. Mallet, F., Millo, J.V.: Boundness Issues in CCSL Specifications. In: ICFEM 2013. LNCS, vol. 8144, pp. 20–35. Springer (Oct 2013). https://doi.org/10.1007/978-3-642-41202-8_3

18. Mallet, F., de Simone, R.: Correctness issues on marte/ccsl constraints. Sci. Comput. Program. **106**(C), 78–92 (Aug 2015). https://doi.org/10.1016/j.scico.2015.03.001

19. Mallet, F., Millo, J.V., de Simone, R.: Safe ccsl specifications and marked graphs. In: (MEMOCODE 2013). pp. 157–166 (2013)

20. de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008). https://doi.org/10.1007/978-3-540-78800-3_24

21. Ndouna, A.R., Frappier, M.: Case Study TCS ASTD. https://github.com/ndounalex/CCSL-to-ASTD-translation (2024)

22. Nganyewou Tidjon, L., Frappier, M., Leuschel, M., Mammar, A.: Extended Algebraic State-Transition Diagrams. In: 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS). pp. 146–155. Melbourne, Australia (2018)

23. Peraldi-Frati, M., DeAntoni, J.: Scheduling multi clock real time systems: From requirements to implementation. In: 14th IEEE ISORC 2011. pp. 50–57. IEEE CS (2011). https://doi.org/10.1109/ISORC.2011.16

24. Rivière, P., Singh, N.K., Ait-Ameur, Y.: Reflexive event-b: Semantics and correctness the EB4EB framework. IEEE Trans. Reliab. **73**(2), 835–850 (2024). https://doi.org/10.1109/TR.2022.3219649

25. Spönemann, M., Schulze, C.D., Motika, C., Schneider, C., von Hanxleden, R.: KIELER: building on automatic layout for pragmatics-aware modeling. In: Kelleher, C., Burnett, M.M., Sauer, S. (eds.) 2013 IEEE VL/HCC. pp. 195–196. IEEE Computer Society (2013). https://doi.org/10.1109/VLHCC.2013.6645265

26. Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., André, É.: Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Softw. Eng. Methodol. **22**(1), 3:1–3:29 (2013). https://doi.org/10.1145/2430536.2430537
27. Suryadevara, J., Seceleanu, C., Mallet, F., Pettersson, P.: Verifying marte/ccsl mode behaviors using uppaal. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) Software Engineering and Formal Methods. pp. 1–15. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)

28. Winskel, G.: Event structures. In: Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course. LNCS, vol. 255, pp. 325–392. Springer (1986). https://doi.org/10.1007/3-540-17906-2_31

29. Zhang, M., Song, F., Mallet, F., Chen, X.: SMT-based bounded schedulability analysis of the clock constraint specification language. In: Hähnle, R., van der Aalst, W. (eds.) FASE. pp. 61–78. Springer (2019)