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

HAL
open science

# Formal Specification of the HILECOP Model-to-text
Transformation

Vincent Iampietro

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

## To cite this version:

Vincent Iampietro. Formal Specification of the HILECOP Model-to-text Transformation. 2022. hal-03661152

HAL Id: hal-03661152

https://hal.science/hal-03661152

Preprint submitted on 9 May 2022

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.

Public Domain
# Formal specification of the HILECOP model-to-text transformation

VINCENT IAMPIETRO

May 9, 2022

## 1 Introduction

This document serves as a reference for the formal specification of the HILECOP model-to-text transformation. HILECOP is a methodology for the design and synthesis of safety-critical digital systems [1]. Many elements used in the following definitions are introduced in the following thesis [2].

## 2 Preliminary definitions

The HILECOP model-to-text transformation (HM2T) generates a $\mathcal{H}$-VHDL design [2, p.65] out of an SITPN model [2, p.37]. It also generates a structure that relates the elements of the SITPN model to the elements of the $\mathcal{H}$-VHDL design. This structure is called a SITPN-to-$\mathcal{H}$-VHDL binder. Its formal definition is as follows:

**Definition 1** (SITPN-to-$\mathcal{H}$-VHDL design binder). *Given a sitpn $\in$ SITPN and a $\mathcal{H}$-VHDL design $d \in$ design, a SITPN-to-$\mathcal{H}$-VHDL binder $\gamma \in$ WM(sitpn, $d$) is a tuple <PMap, TMap, CMap, AFMap> where:*

* $PMap \in P \rightarrow \{id_p | \text{comp}(id_p, \text{place}, g, i, o) \in d.\text{beh}\}$

* $TMap \in T \rightarrow \{id_t | \text{comp}(id_t, \text{transition}, g, i, o) \in d.\text{beh}\}$

* $CMap \in C \rightarrow \{id_c | (\text{in}, id_c, \text{bool}) \in d.\text{ports}\}$

* $AFMap \in A \cup F \rightarrow \{id_{af} | (\text{out}, id_{af}, \text{bool}) \in d.\text{ports}\}$

**Notation 1.** For a given binder $\gamma$ and an element of an SITPN structure $e \in P \cup T \cup C \cup A \cup F$, we write $\gamma(e)$ where $e$ is looked up in the appropriate function. For instance, for a given $f \in F$, $\gamma(f)$ is a shorthand notation for $AFMap(f)$ where $\gamma = <..., AFMap>$.

While presenting the specification of the HM2T, we refer to two pre-defined designs, namely: the place and transition designs. The details of the implementation of the place and transition designs in $\mathcal{H}$-VHDL are given in Appendices A and B. The HILECOP design store has been specifically defined for the elaboration and simulation the $\mathcal{H}$-VHDL designs generated by the HM2T. It holds the definitions of the place and transition designs.
# 3 Formal specification

In the following section, we present the formal specification of the HM2T. The specification is a relation between the inputs of the HM2T, namely a SITPN model and a bounding function, and the possible outputs which can be either a pair composed of a $\mathcal{H}$-VHDL design and a SITPN-to-$\mathcal{H}$-VHDL binder or the error value. The relation is written $HM2T_{\text{spec}} \subseteq \text{SITPN} \times (P \to \mathbb{N}) \times ((\text{design} \times \text{WM}(\text{sitpn}, d)) \cup \{\text{err}\})$.

**Definition 2** (HILECOP model-to-text transformation specification). For all SITPN model $\text{sitpn} \in \text{SITPN}$, bounding function $b \in P \to \mathbb{N}$, $\mathcal{H}$-VHDL design $d \in \text{design}$, and SITPN-to-$\mathcal{H}$-VHDL binder $\gamma \in \text{WM}(\text{sitpn}, d)$, we have $HM2T_{\text{spec}}(\text{sitpn}, b, (d, \gamma))$ if:

1. Design *d* has an empty generic clause: $d.gens = \emptyset$.

2. The number of input ports of the design is equal to the number of conditions of the SITPN model: $|\{id | (\text{in}, id, \tau) \in d.\text{ports}\}| = |\mathcal{C}|$.

3. The number of output ports of the design is equal to the number of actions and functions of the SITPN model: $|\{id | (\text{out}, id, \tau) \in d.\text{ports}\}| = |\mathcal{A} \cup \mathcal{F}|$.

4. Design *d* is elaborable in the context of the HILECOP design store and given an empty dimensioning function: $\exists \Delta \in \text{ElDesign}, \sigma_e \in \Sigma \text{ s.t. } \mathcal{D}_{\mathcal{H}}, \emptyset \vdash d \xrightarrow{\text{elab}} \Delta, \sigma_e$.

5. All design instantiation statement in the design's behavior either creates a PDI or a TDI: $\forall id_c, id_e, g, i, o \text{ s.t. } \text{comp}(id_c, id_e, g, i, o) \in d.\text{beh}, id_e = \text{place} \lor id_e = \text{transition}$.

6. The actions and functions processes are the only two processes in the design's behavior: $\forall id_p, \text{vars}, \text{ss} \text{ s.t. } \text{ps}(id_p, \text{vars}, \text{ss}) \in d.\text{beh}, id_p = \text{actions} \lor id_p = \text{functions}$.

7. All the fields of the SITPN-to-$\mathcal{H}$-VHDL binder are bijective functions: $\text{PMap}(\gamma)$ is bijective, $\text{TMap}(\gamma)$ is bijective, ...

8. For all place of the input SITPN model, there exists a corresponding place design instance (PDI) identified through $\gamma$ in the behavior of the output design: $\forall p \in P, \exists g_p, i_p, o_p \text{ s.t. } \text{comp}(\gamma(p), \text{place}, g_p, i_p, o_p) \in d.\text{beh}$.

9. For all place of the input SITPN model and its corresponding PDI, the generic map of the PDI holds the following associations: 
   $\forall p \in P, g_p, i_p, o_p, \text{comp}(\gamma(p), \text{place}, g_p, i_p, o_p) \in d.\text{beh} \Rightarrow$
   $g_p = \{(\text{mm} \Rightarrow b(p)), (\text{ian} \Rightarrow \begin{cases} 1 & \text{if } \text{input}(p) = \emptyset \\ |\text{input}(p)| & \text{otherwise} \end{cases}), (\text{oan} \Rightarrow \begin{cases} 1 & \text{if } \text{output}(p) = \emptyset \\ |\text{output}(p)| & \text{otherwise} \end{cases})\}$
   where $\text{input}(p) = \{t \mid \text{post}(t, p) = \lfloor\omega\rfloor\}$, the set of input transitions of place *p*, and $\text{output}(p) = \{t \mid \text{pre}(p, t) = \lfloor(\omega, a)\rfloor\}$, the set of output transitions of place *p*.

10. For all place of the input SITPN model and its corresponding PDI, there is an association between the *im* input port and the initial marking of the place in the input port map of the PDI: $\forall p \in P, g_p, i_p, o_p, \text{comp}(\gamma(p), \text{place}, g_p, i_p, o_p) \in d.\text{beh} \Rightarrow (\text{im} \Rightarrow M_0(p)) \in i_p$.
11. For all place of the SITPN model with no input transition, the input port map of the corresponding PDI includes the following associations:

$$
\begin{align*}
\forall p \in P, g_p, i_p, o_p, \\
\quad \mathit{input}(p) &= \emptyset \Rightarrow \\
\quad \mathit{comp}(\gamma(p), \mathit{place}, g_p, i_p, o_p) &\in d.\mathit{beh} \Rightarrow \\
\quad \{ (\mathit{iaw}(0) \Rightarrow 0), (\mathit{itf}(0) \Rightarrow \mathit{false}) \} &\subseteq i_p.
\end{align*}
$$

12. For all place of the SITPN model with no output transition, the input port map and output port map of the corresponding PDI includes the following associations:

$$
\begin{align*}
\forall p \in P, g_p, i_p, o_p, \\
\quad \mathit{output}(p) &= \emptyset \Rightarrow \\
\quad \mathit{comp}(\gamma(p), \mathit{place}, g_p, i_p, o_p) &\in d.\mathit{beh} \Rightarrow \\
\quad \{ (\mathit{oaw}(0) \Rightarrow 0), (\mathit{oat}(0) \Rightarrow \mathit{basic}), (\mathit{otf}(0) \Rightarrow \mathit{false}) \} &\subseteq i_p \\
\quad \wedge \{ (\mathit{oav} \Rightarrow \mathit{open}), (\mathit{pah} \Rightarrow \mathit{open}), (\mathit{rtt} \Rightarrow \mathit{open}) \} &\subseteq o_p.
\end{align*}
$$

13. For all place of the SITPN model with no action, the marked output port is left unconnected in the output port map of the corresponding PDI:

$$
\begin{align*}
\forall p \in P, g_p, i_p, o_p, \\
\quad \mathit{acts}(p) &= \emptyset \Rightarrow \\
\quad \mathit{comp}(\gamma(p), \mathit{place}, g_p, i_p, o_p) &\in d.\mathit{beh} \Rightarrow \\
\quad (\mathit{marked} \Rightarrow \mathit{open}) &\in o_p
\end{align*}
$$

where $\mathit{acts}(p) = \{a \mid A(p, a) = \text{true}\}$, the set of actions associated with place $p$.

14. For all transition of the input SITPN model, there exists a corresponding TDI identified through $\gamma$ in the behavior of the output design:

$$
\forall t \in T, \exists g_t, i_t, o_t \text{ s.t. } \mathbf{comp}(\gamma(t), \mathbf{transition}, g_t, i_t, o_t) \in d.\mathbf{beh}.
$$

15. For all transition of the input SITPN model and its corresponding TDI, the generic map of the TDI holds the following associations:

$$
\begin{align*}
\forall t \in T, g_t, i_t, o_t, \quad \mathit{comp}(\gamma(t), \mathit{transition}, g_t, i_t, o_t) &\in d.\mathit{beh} \Rightarrow \\
g_t = \{ (\mathit{tt} \Rightarrow \left\{ \begin{array}{@{}l@{}} \mathit{NOT\_TEMPORAL} \text{ if } t \notin \mathit{dom}(I_s) \\ \mathit{TEMPORAL\_A\_A} \text{ if } I_s(t) = [a, a] \\ \mathit{TEMPORAL\_A\_B} \text{ if } I_s(t) = [a, b] \\ \mathit{TEMPORAL\_A\_INF} \text{ if } I_s(t) = [a, \infty] \end{array} \right. ), (\mathit{mtc} \Rightarrow \left\{ \begin{array}{@{}l@{}} 1 \text{ if } t \notin \mathit{dom}(I_s) \\ \text{b if } I_s(t) = [a, b] \\ \text{a if } I_s(t) = [a, \infty] \end{array} \right. ), \\
(\mathit{ian} \Rightarrow \left\{ \begin{array}{@{}l@{}} 1 \text{ if } \mathit{input}(t) = \emptyset \\ |\mathit{input}(t)| \text{ otherwise} \end{array} \right. ), (\mathit{cn} \Rightarrow \left\{ \begin{array}{@{}l@{}} 1 \text{ if } \mathit{conds}(t) = \emptyset \\ |\mathit{conds}(t)| \text{ otherwise} \end{array} \right. \}.
\end{align*}
$$

where $\mathit{input}(t) = \{p \mid \mathit{pre}(p, t) = \lfloor(\omega, a)\rfloor\}$, the set of input places of transition $t$, and $\mathit{conds}(t) = \{c \mid \mathcal{C}(t, c) = 1 \lor \mathcal{C}(t, c) = -1\}$, the set of conditions associated with transition $t$.
16. For all transition of the input SITPN model and its corresponding TDI, the input port map of the TDI holds the following associations:

$$
\forall t \in T, g_t, i_t, o_t, \\
\quad \text{comp}(\gamma(t), \mathbf{transition}, g_t, i_t, o_t) \in d.\mathbf{beh} \Rightarrow \\
\quad \left\{ \begin{array}{l} (A \Rightarrow \left\{ \begin{array}{l} 0 \text{ if } t \notin \text{dom}(I_s) \\ l(I_s(t)) \text{ otherwise} \end{array} \right\}), (B \Rightarrow \left\{ \begin{array}{l} 0 \text{ if } t \notin \text{dom}(I_s) \lor u(I_s(t)) = \infty \\ u(I_s(t)) \text{ otherwise} \end{array} \right\}} \subseteq i_t. \end{array} \right.
$$

17. For all transition of the input SITPN model with no input place, the input port map and output port map of the corresponding TDI holds the following associations:

$$
\begin{align*}
\forall t \in T, g_t, i_t, o_t, & \\
\mathbf{input}(t) = \emptyset & \Rightarrow \\
\mathbf{comp}(\gamma(t), \mathbf{transition}, g_t, i_t, o_t) & \in d.\mathbf{beh} \Rightarrow \\
& \quad (\exists id_s \text{ s.t. } (id_s, \mathbf{bool}) \in d.\mathbf{sigs} \land (\mathbf{rt}(0) \Rightarrow id_s) \in i_t \land (\mathbf{fired} \Rightarrow id_s) \in o_t) \\
& \quad \land \{(\mathbf{iav}(0) \Rightarrow \mathbf{true}), (\mathbf{pah}(0) \Rightarrow \mathbf{true})\} \subseteq i_t.
\end{align*}
$$

18. For all transition of the input SITPN model with no condition, the input port map of the corresponding TDI holds the following association:

$$
\forall t \in T, g_t, i_t, o_t, \\
\quad \mathbf{conds}(t) = \emptyset \Rightarrow \\
\quad \mathbf{comp}(\gamma(t), \mathbf{transition}, g_t, i_t, o_t) \in d.\mathbf{beh} \Rightarrow \\
\quad (\mathbf{ic}(0) \Rightarrow \mathbf{true}) \in i_t.
$$

19. For all post arc of the input SITPN model, the TDI and PDI corresponding to the source transition and target place of the arc are connected as follows:

$$
\begin{align*}
\forall t \in T, p \in P, g_t, i_t, o_t, g_p, i_p, o_p, \omega \in \mathbb{N}^*, \\
\quad \text{post}(t, p) = \lfloor \omega \rfloor &\Rightarrow \\
\quad \text{comp}(\gamma(t), \text{transition}, g_t, i_t, o_t) &\in d.\text{beh} \Rightarrow \\
\quad \text{comp}(\gamma(p), \text{place}, g_p, i_p, o_p) &\in d.\text{beh} \Rightarrow \\
\quad \exists i \in [0, |\text{input}(p)| - 1] \text{ s.t. } (\text{iaw}(i) \Rightarrow \omega) &\in i_p \\
\quad \wedge \exists id_s \text{ s.t. } (id_s, \text{bool}) \in d.\text{sigs} \wedge (\text{fired} \Rightarrow id_s) \in o_t \wedge (\text{itf}(i) \Rightarrow id_s) \in i_p.
\end{align*}
$$

20. For all pre arc of the input SITPN model, the PDI and TDI corresponding to the source place and target
transition of the arc are connected as follows:

$$
\begin{align*}
& \forall t \in T, p \in P, g_t, i_t, o_t, g_p, i_p, o_p, \omega \in \mathbb{N}^*, a \in \{\text{basic, test, inhib}\}, \\
& \text{pre}(p, t) = \lfloor (\omega, a) \rfloor \Rightarrow \\
& \quad \text{comp}(\gamma(t), \text{transition}, g_t, i_t, o_t) \in \text{d.beh} \Rightarrow \\
& \quad \text{comp}(\gamma(p), \text{place}, g_p, i_p, o_p) \in \text{d.beh} \Rightarrow \\
& \quad \exists i \in [0, |\text{output}(p)| - 1] \text{ s.t. } \{(\text{oaw}(i) \Rightarrow \omega), (\text{oat}(i) \Rightarrow a)\} \subseteq i_p \\
& \quad \wedge \exists j \in [0, |\text{input}(t)| - 1], id_{av}, id_{rt}, id_{frd}, id_{pah} \text{ s.t.} \\
& \quad \quad \{(id_{av}, \text{bool}), (id_{rt}, \text{bool}), (id_{frd}, \text{bool}), (id_{pah}, \text{bool})\} \subseteq \text{d.sigs} \\
& \quad \wedge (\text{oav}(i) \Rightarrow id_{av}) \in o_p \wedge (\text{iav}(j) \Rightarrow id_{av}) \in i_t \\
& \quad \wedge (\text{rtt}(i) \Rightarrow id_{rt}) \in o_p \wedge (\text{rt}(j) \Rightarrow id_{rt}) \in i_t \\
& \quad \wedge (\text{otf}(i) \Rightarrow id_{frd}) \in i_p \wedge (\text{fired} \Rightarrow id_{frd}) \in o_t \\
& \quad \wedge (\text{pah}(i) \Rightarrow id_{frd}) \in o_p \\
& \quad \wedge (a = \text{test} \lor a = \text{inhib} \lor \text{confl}(p) = \emptyset \Rightarrow (\text{pah}(j) \Rightarrow \text{true}) \in i_t) \\
& \quad \wedge (a = \text{basic} \land \text{confl}(p) \neq \emptyset \text{ or } \text{err} \Rightarrow (\text{pah}(j) \Rightarrow id_{pah}) \in i_t).
\end{align*}
$$

where $\text{confl} \in P \to 2^T \cup \{\text{err}\}$ takes a place $p$ as input and yields either an error or an ordered set of transitions computed as follows:

(a) If all conflicts between the output transitions of $p$ are solved by mutual exclusion, or if the set of conflicting transitions of $p$ is a singleton, then $\text{confl}$ returns an empty set.

(b) Otherwise, the function tries to establish a total ordering over the set of conflicting transitions of $p$ w.r.t the firing priority relation:

* If no such ordering can be established (in that case, the firing priority relation is ill-formed, and the input SITPN is not well-defined), $\text{confl}$ returns the `err` value.

* Otherwise, the function returns the set in a decreasing priority order.

21. For all place of the input SITPN model for which conflicts in its output transitions are not solved by mutual exclusion, the port indices of the corresponding PDI reflect the priority order established between
the conflicting output transitions:

$$
\begin{align*}
& \forall p \in P, t, t' \in \mathbf{confl}(p), g_p, i_p, o_p, g_t, i_t, o_t, g_{t'}, i_{t'}, o_{t'}, \\
& t \succ t' \Rightarrow \\
& \quad \mathbf{comp}(\gamma(p), \mathbf{place}, g_p, i_p, o_p) \in \mathbf{d.beh} \Rightarrow \\
& \quad \mathbf{comp}(\gamma(t), \mathbf{transition}, g_t, i_t, o_t) \in \mathbf{d.beh} \Rightarrow \\
& \quad \mathbf{comp}(\gamma(t'), \mathbf{transition}, g_{t'}, i_{t'}, o_{t'}) \in \mathbf{d.beh} \Rightarrow \\
& \quad (\forall i, j \in \mathbb{N}, id_{frd}, id_{frd'}, id_s, id_{s'}, name_t, name_{t'}, id_{out}, \\
& \qquad \mathbf{(fired} \Rightarrow id_{frd}) \in o_t \Rightarrow \\
& \qquad \mathbf{(fired} \Rightarrow id_{frd'}) \in o_{t'} \Rightarrow \\
& \qquad \{ (\mathbf{otf}(i) \Rightarrow id_{frd}), (\mathbf{otf}(j) \Rightarrow id_{frd'}) \} \subseteq i_p \Rightarrow \\
& \qquad (name_t \Rightarrow id_s) \in i_t \Rightarrow \\
& \qquad (name_{t'} \Rightarrow id_{s'}) \in i_{t'} \Rightarrow \\
& \qquad \{ (id_{out}(i) \Rightarrow id_s), (id_{out}(j) \Rightarrow id_{s'}) \} \subseteq o_p \Rightarrow \\
& \qquad i < j)
\end{align*}
$$

22. There exists an **actions** process that assigns a value to the output port representing the activation status of the actions (referred to as action ports) of the input SITPN model:

$$
\exists ss_{ra}, ss_a \text{ s.t. } \mathbf{ps}(\mathbf{actions}, \emptyset, \mathbf{rst}\{ss_{ra}\} \text{else}\{\mathbf{falling}\{ss_a\}\}) \in \mathbf{d.beh} \text{ and}
$$

(a) The length of the `ss ra` and `ss a` sequences is equal to the number of actions of the input SITPN model:

$$
|ss_{ra}| = |ss_a| = |\mathcal{A}| \text{ where } |ss| = \begin{cases} |ss_1| + |ss_2| & \text{if } ss = ss_1; ss_2 \\ 1 & \text{otherwise} \end{cases}
$$

(b) During the initialization, all action ports are assigned to **false** by the **actions** process:

$$
\forall a \in \mathcal{A}, \gamma(a) \Leftarrow \mathbf{false} \in ss_{ra}
$$

(c) An action port corresponding to an action associated with no place is assigned to **false** during the falling edge phase:

$$
\forall a \in \mathcal{A} \text{ s.t. } \mathbf{pls}(a) = \emptyset, \gamma(a) \Leftarrow \mathbf{false} \in ss_a \text{ where } \mathbf{pls}(a) = \{p \mid \mathcal{A}(p, a) = \mathbf{true}\}, \text{ the set of places associated with action a.}
$$

(d) Otherwise, the value of the action port is the result of the Boolean sum between the **marked** output port of all PDIs representing the places associated with the corresponding action:

$$
\begin{align*}
\forall a \in \mathcal{A}, \mathbf{pls}(a) \neq \emptyset \Rightarrow \\
\quad \exists e_{or} \text{ s.t. } \gamma(a) \Leftarrow e_{or} \in ss_a \wedge \mathbf{is\_bsum}(e_{or}, |\mathbf{pls}(a)|) \\
\wedge \forall p \in \mathbf{pls}(a), g_p, i_p, o_p, \\
\quad \quad \mathbf{comp}(\gamma(p), \mathbf{place}, g_p, i_p, o_p) \in \mathbf{d.beh} \Rightarrow \\
\quad \quad \exists id_m \text{ s.t. } (id_m, \mathbf{bool}) \in \mathbf{d.sigs} \wedge id_m \in e_{or} \wedge (\mathbf{marked} \Rightarrow id_m) \in o_p
\end{align*}
$$

$$
\text{where } \mathbf{is\_bsum} \text{ is defined as follows: } \frac{e \in \{id, b\}}{\mathbf{is\_bsum}(e, 1)} \quad \frac{\mathbf{is\_bsum}(e_1, n) \quad \mathbf{is\_bsum}(e_2, m)}{\mathbf{is\_bsum}(\mathbf{or}(e_1, e_2), n + m)}
$$
23. There exists an **functions** process that assigns a value to the output port representing the execution status of the functions (referred to as function ports) of the input SITPN model:

$$ \exists ss_{rf}, ss_f \text{ s.t. } \texttt{ps(functions, \emptyset, rst(ss_{rf})else{rising(ss_f)})} \in d.\texttt{beh and} $$

(a) The length of the $ss_{rf}$ and $ss_f$ sequences is equal to the number of functions of the input SITPN model:

$$ |ss_{rf}| = |ss_f| = |\mathcal{F}| $$

(b) During the initialization, all function ports are assigned to **false** by the **functions** process:

$$ \forall f \in \mathcal{F}, \gamma(f) \Leftarrow \texttt{false} \in ss_{rf} $$

(c) An function port corresponding to an function associated with no transition is assigned to **false** during the rising edge phase:

$$ \forall f \in \mathcal{F} \text{ s.t. } \texttt{trs}(f) = \emptyset, \gamma(f) \Leftarrow \texttt{false} \in ss_f \text{ where } \texttt{trs}(f) = \{t \mid \mathcal{F}(t, f) = \texttt{true}\}, \text{ the set of transitions associated with function } f. $$

(d) Otherwise, the value of the function port is the result of the Boolean sum between the **fired** output port of all TDIs representing the transitions associated with the considered function:

$$ \begin{array}{l} \forall f \in \mathcal{F}, \texttt{trs}(f) \neq \emptyset \Rightarrow \\ \quad \exists e_{or} \text{ s.t. } \gamma(f) \Leftarrow e_{or} \in ss_f \wedge \texttt{is\_bsum}(e_{or}, |\texttt{trs}(f)|) \\ \wedge \forall t \in \texttt{trs}(f), g_t, i_t, o_t, \\ \quad \quad \texttt{comp}(\gamma(t), \texttt{transition}, g_t, i_t, o_t) \in d.\texttt{beh} \Rightarrow \\ \quad \quad \exists id_m \text{ s.t. } (id_m, \texttt{bool}) \in d.\texttt{sigs} \wedge id_m \in e_{or} \wedge (\texttt{fired} \Rightarrow id_m) \in o_t \end{array} $$

24. For all association between a transition and a condition, the input port reflecting the Boolean value of the given condition (referred to as a condition port) is connected as follows to the input port map of the TDI corresponding to the associated transition:

$$ \begin{array}{l} \forall t \in T, g_t, i_t, o_t, c \in \mathcal{C}, \\ \quad \texttt{comp}(\gamma(t), \texttt{transition}, g_t, i_t, o_t) \in d.\texttt{beh} \Rightarrow \\ \quad (\mathbb{C}(t, c) = 1 \Rightarrow \exists i \in [0, |\texttt{conds}(t)| - 1] \text{ s.t. } (\texttt{ic}(i) \Rightarrow \gamma(c)) \in i_t) \\ \quad (\mathbb{C}(t, c) = -1 \Rightarrow \exists i \in [0, |\texttt{conds}(t)| - 1] \text{ s.t. } (\texttt{ic}(i) \Rightarrow \texttt{not}(\gamma(c))) \in i_t). \end{array} $$

To conclude the definition of the $HM2T_{spec}$ relation, we have $HM2T_{spec}(sitpn, b, \texttt{err})$ if sitpn is not a well-defined SITPN model [2].
A The place design in abstract *H*-VHDL syntax

1

2

3 -- Generic constant declarations

4 gens = {

5 (input_arcs_number, nat(0, NATMAX), 1),

6 (output_arcs_number, nat(0, NATMAX), 1),

7 (maximal_marking, nat(0, NATMAX), 1)},

8

9 -- Port declarations

10 ports = {

11 (in, initial_marking, nat(0, maximal_marking)),

12 (in, input_arcs_weights, array (nat(0, 255), 0, sub(input_arcs_number, 1))),

13 (in, output_arcs_types, array (nat(0, 2), 0, sub(output_arcs_number, 1))),

14 (in, output_arcs_weights, array (nat(0, 2), 0, sub(output_arcs_number, 1))),

15 (in, input_transitions_fired, array (bool, 0, sub(input_arcs_number, 1))),

16 (in, output_transitions_fired, array (bool, 0, sub(output_arcs_number, 1))),

17 (out, output_arcs_valid, array (bool, 0, sub(output_arcs_number, 1))),

18 (out, priority_authORIZAtions, array (bool, 0, sub(output_arcs_number, 1))),

19 (out, reinit_transitions_time, array (bool, 0, sub(output_arcs_number, 1))),

20 (out, marked, bool)},

21

22 -- Internal signal declarations

23 sigs ={(s_input_tokens_sum, nat(0, maximal_marking)),

24 (s_marking, nat(0, maximal_marking)),

25 (s_output_tokens_sum, nat(0, maximal_marking))};

26

27 -- Behavior

28 beh =

29 ps (input_tokens_sum,

30 {(v_tokens_sum, nat(0, maximal_marking))};

31 v_tokens_sum := 0;

32 for (i, 0, sub(input_arcs_number, 1)){

33 if (input_transitions_fired(i)) {
34 v_tokens_sum := add(v_tokens_sum, input_arcs_weights(i))
35 } else { null }
36 };

35
36
37

36
37

s_input_tokens_sum $\leftarrow$ v_tokens_sum)

38
||

39 ps (output_tokens_sum,

40 {(v_tokens_sum, nat(0, maximal_marking))};

41 v_tokens_sum := 0;

42 for (i, 0, sub(output_arcs_number, 1)) {

43 if (and(output_transitions_fired(i), eq(output_arcs_types(i), 0))) {

44 v_tokens_sum := add(v_tokens_sum, output_arcs_weights(i))

45 } else { null }

46
47

s_output_tokens_sum $\leftarrow$ v_tokens_sum)

47
```
48 ||
49 ps (marking, Ø,
50 rst { s_marking ⇌ initial_marking }
51 else {
52     rising {
53         s_marking ⇌ add(s_marking, sub(s_input_tokens_sum, s_output_tokens_sum))
54     }
55 })
56 ||
57 ps (determine_marked, Ø, marked ⇌ gt(s_marking, 0))
58 ||
59 ps (marking_validation_evalutation, Ø,
60     for (i, 0, sub(output_arcs_number, 1)) {
61         output_arcs_valid(i) ⇌
62             or(and(or(eq(output_arcs_types(i), 0),
63                 eq(output_arcs_types(i), 1)),
64                 ge(s_marking, output_arcs_weights(i)))),
65         and(eq(output_arcs_types(i), 2),
66             lt(s_marking, output_arcs_weights(i))))
67     })
68 ||
69 ps (priority_evalutation,
70     {(v_saved_output_tokens_sum, nat(0, maximal_marking))},
71     v_saved_output_tokens_sum := 0;
72     for (i, 0, sub(output_arcs_number, 1)) {
73         priority_authORIZATIONS(i) ⇌ ge(s_marking, add(v_saved_output_tokens_sum, output_arcs_weights(i));
74         if (and(output_transitions_fired(i), eq(output_arcs_types(i), 0))) {
75             v_saved_output_tokens_sum := add(v_saved_output_tokens_sum, output_arcs_weights(i))
76         } else { null }
77     })
78 ||
79 ps (reinit_transitions_time_evalutation, Ø,
80     rst {
81         for (i, 0, sub(output_arcs_number, 1)) {
82             reinit_transitions_time(i) ⇌ false
83         }
84     } else {
85         rising {
86             for (i, 0, sub(output_arcs_number, 1)) {
87                 reinit_transitions_time(i) ⇌
88                 or(and(and(or(eq(output_arcs_types(i), 0),
89                     eq(output_arcs_types(i), 1)),
90                     lt(sub(s_marking, s_output_tokens_sum),
91                     output_arcs_weights(i))))
92             }
93         }
94     }
95 }
```
96
}
97
}

<caption>Listing 1: The place design in *H*-VHDL abstract syntax.</caption>
B The transition design in abstract *H*-VHDL syntax

1

2

3 -- Generic constant declarations

4 gens={

5 (transition_type, nat(0, 3), 0),

6 (input_arcs_number, nat(0, NATMAX), 1),

7 (conditions_number, nat(0, NATMAX), 1),

8 (maximal_time_counter, nat(0, NATMAX), 1)},

9

10 -- Port declarations

11 ports=

12 (in, input_conditions, array(bool, 0, sub(conditions_number, 1))),

13 (in, time_A_value, nat(0, maximal_time_counter)),

14 (in, time_B_value, nat(0, maximal_time_counter)),

15 (in, input_arcs_valid, array(bool, 0, sub(input_arcs_number, 1))),

16 (in, reinit_time, array(bool, 0, sub(input_arcs_number, 1))),

17 (in, priority_authORIZAtions, array boolean, 0, sub(input_arcs_number, 1))),

18 (out, fired, bool)},

19

20 -- Internal signal declarations

21 sigs=

22 (s_condition Combination, bool),

23 (s_enabled, bool),

24 (s_firable, bool),

25 (s_firing, bool),

26 (s_priority, bool),

27 (s_reinit, bool),

28 (s_time_counter, nat(0, maximal_time_counter)),

29

30 -- Behavior

31 beh=

32 ps (condition_evalUation, {(v_internal_condition, bool)},

33 v_internal_condition := true;

34 for (i, 0, sub(conditions_number, 1)) {
35 v_internal_condition := and(v_internal_condition, input_conditions(i))
36 };

37 s_condition Combination ← v_internal_condition)

38 ||

39 ps (enable_evalUation, {(v_internal_enabled, bool)},

40 v_internal_enabled := true;

41 for (i, 0, sub(input_arcs_number, 1)) {
42 v_internal_enabled := and(v_internal_enabled, input_arcs_valid(i))
43 };

44 s_enabled ← v_internal_enabled)

45 ||

46 ps (reinit_time_counter_evalUation, {(v_internal_reinit_time_counter, bool)},

47 v_internal_reinit_time_counter := false;
48 for (i, 0, sub(input_arcs_number, 1)) {
49     v_internal_reinit_time_counter := or(v_internal_reinit_time_counter, reinit_time(i))
50 };
51 s_reinit_time_counter := v_internal_reinit_time_counter)

52 ||

53 ps (time_counter, ∅,
54     rst { s_time_counter ← 0 }

55 else {

56     falling {
57         if (and(s_enabled, neq(transition_type, 0))) {
58             if (eq(s_reinit_time_counter, false)) {
59                 if (s_time_counter < maximal_time_counter) {
60                     s_time_counter ← s_time_counter + 1
61                 } else { null }
62             }
63         } else { s_time_counter ← 1 }
64     }
65     else { s_time_counter ← 0 }
66 };

67 })

68 ||

69 ps (firing_condition_evaluation, ∅,

70     s_firing_condition ←
71     s_condition Combination
72     and s_enabled
73     and (eq(transition_type, 0)
74         or (eq(s_reinit_time_counter, false)
75             and ((eq(transition_type, 1)
76                 and ge(s_time_counter, sub(time_A_value, 1))
77                 and (s_time_counter < time_B_value)))
78             or (eq(transition_type, 2)
79                 and eq(s_time_counter, sub(time_A_value, 1))))
80             or (eq(transition_type, 3)
81                 and ge(s_time_counter, sub(time_A_value, 1)))))
82         or (s_reinit_time_counter
83             and neq(transition_type, 0)
84             and eq(time_A_value, 1))))

81

82

83 ||

84 ||
85     ps (priority_authorization_evaluation, {(v_priority Combination, bool)},
86         v_priority Combination := true;
87     for (i, 0, sub(input_arcs_number, 1)) {
88         v_priority Combination := and(v_priority Combination, priority_autherizations(i))
89     };
90     s_priority Combination ← v_priority Combination)

89

90
91
92
93 ||
94     ps (firable, ∅,
95         rst { s_firable ← false }
96     else { falling { s_firable ← s_firing_condition } })
97 ||

90

91

92

93

94

95

96

97

98

99

100

101 ||

102 ||
103     ps (priority_authorization_evaluation, {(v_priority Combination, bool)},
104         v_priority Combination := true;
105     for (i, 0, sub(input_arcs_number, 1)) {
106         v_priority Combination := and(v_priority Combination, priority_autherizations(i))
107     };
108     s_priority Combination ← v_priority Combination)

104

105

106

107

108

109

110 ||

111 ||
112     ps (firable, ∅,
113         rst { s_firable ← false }
114     else { falling { s_firable ← s_firing_condition } })
115 ||

113

114

115

116 ||
Listing 2: The transition design in $\mathcal{H}$-VHDL abstract syntax.
C Generic constant and signal names reference

<table><caption>Table 1: Constants and signals reference for the *H-VHDL* transition and place designs. In the *Category* column, T (resp. P) indicates a generic constant, input port, output port or internal signal defined in the *transition* (resp. *place*) design.</caption><caption>Generic constants and signals reference</caption><thead><tr><th>Full name</th><th>Alias</th><th>Category</th><th>Type</th></tr></thead><tbody><tr><td>input_arcs_number</td><td>ian</td><td>generic constant (T)</td><td>nat(0, NATMAX)</td></tr><tr><td>transition_type</td><td>tt</td><td>generic constant (T)</td><td>{not_temp, temp_a_b, temp_a_a, temp_a_inf}</td></tr><tr><td>conditions_number</td><td>cn</td><td>generic constant (T)</td><td>nat(0, NATMAX)</td></tr><tr><td>maximal_time_counter</td><td>mtc</td><td>generic constant (T)</td><td>nat(0, NATMAX)</td></tr><tr><td>time_A_value</td><td>A</td><td>input port (T)</td><td>nat(0, mtc)</td></tr><tr><td>time_B_value</td><td>B</td><td>input port (T)</td><td>nat(0, mtc)</td></tr><tr><td>input_conditions</td><td>ic</td><td>input port (T)</td><td>array(bool, 0, cn - 1)</td></tr><tr><td>reinit_time</td><td>rt</td><td>input port (T)</td><td>array(bool, 0, ian - 1)</td></tr><tr><td>input_arcs_valid</td><td>iav</td><td>input port (T)</td><td>array(bool, 0, ian - 1)</td></tr><tr><td>priority_authORIZATIONS</td><td>pah</td><td>input port (T)</td><td>array(bool, 0, ian - 1)</td></tr><tr><td>fired</td><td>f</td><td>output port (T)</td><td>bool</td></tr><tr><td>s_condition Combination</td><td>scc</td><td>internal signal (T)</td><td>bool</td></tr><tr><td>s_reinit_time_counter</td><td>sRTC</td><td>internal signal (T)</td><td>bool</td></tr><tr><td>s_priority Combination</td><td>spc</td><td>internal signal (T)</td><td>bool</td></tr><tr><td>s_firable</td><td>sfa</td><td>internal signal (T)</td><td>bool</td></tr><tr><td>s_enabled</td><td>se</td><td>internal signal (T)</td><td>bool</td></tr><tr><td>s_time_counter</td><td>STC</td><td>internal signal (T)</td><td>nat(0, mtc)</td></tr><tr><td>s_firing_condition</td><td>SFC</td><td>internal signal (T)</td><td>bool</td></tr><tr><td>input_arcs_number</td><td>ian</td><td>generic constant (P)</td><td>nat(0, NATMAX)</td></tr><tr><td>output_arcs_number</td><td>oan</td><td>generic constant (P)</td><td>nat(0, NATMAX)</td></tr><tr><td>maximal_marking</td><td>mm</td><td>generic constant (P)</td><td>nat(0, NATMAX)</td></tr><tr><td>initial_marking</td><td>im</td><td>input port (P)</td><td>nat(0, mm)</td></tr><tr><td>output_arcs_types</td><td>oat</td><td>input port (P)</td><td>array({basic, test, inhib}, 0, oan - 1)</td></tr><tr><td>output_arcs weights</td><td>oaw</td><td>input port (P)</td><td>array(nat(0, 255), 0, oan - 1)</td></tr><tr><td>output_transitions_fired</td><td>OTF</td><td>input port (P)</td><td>array(bool, 0, oan - 1)</td></tr><tr><td>input_arcs weights</td><td>iav</td><td>input port (P)</td><td>array(nat(0, 255), 0, ian - 1)</td></tr><tr><td>input_transitions_fired</td><td>ITF</td><td>input port (P)</td><td>array(bool, 0, ian - 1)</td></tr><tr><td>output_arcs_valid</td><td>oav</td><td>output port (P)</td><td>array(bool, 0, oan - 1)</td></tr><tr><td>reinit_transitions_time</td><td>rtt</td><td>output port (P)</td><td>array(bool, 0, oan - 1)</td></tr><tr><td>priority_authORIZATIONS</td><td>pah</td><td>output port (P)</td><td>array(bool, 0, oan - 1)</td></tr><tr><td>marked</td><td>m</td><td>output port (P)</td><td>bool</td></tr><tr><td>s_marking</td><td>sm</td><td>internal signal (P)</td><td>nat(0, mm)</td></tr><tr><td>s_output_token_sum</td><td>sots</td><td>internal signal (P)</td><td>nat(0, mm)</td></tr><tr><td>s_input_token_sum</td><td>sits</td><td>internal signal (P)</td><td>nat(0, mm)</td></tr></tbody></table>
References

[1] David Andreu, David Guiraud, and Guillaume Souquet. “A Distributed Architecture for Activating the Peripheral Nervous System”. In: *Journal of Neural Engineering* 6.2 (Apr. 1, 2009), p. 026001. ISSN: 1741-2560, 1741-2552. DOI: 10.1088/1741-2560/6/2/026001. URL: https://iopscience.iop.org/article/10.1088/1741-2560/6/2/026001 (visited on 06/08/2020).

[2] Vincent Iampietro. “Vérification formelle d’une méthodologie pour la conception et la production de systèmes numériques critiques”. Theses. Université Montpellier, Dec. 2021. URL: https://tel.archives-ouvertes.fr/10.7865/tel-020010001