## 5 System Model
### SDN Model
Furthermore, we consider the bijection \(f_{pflow}:PFLOW\mapsto MATCH\), that is each \(pflow\) corresponds to a \(match\in MATCH\) denoted by \(pflow\triangleq match\). * Forwarding paths: A finite set of forwarding paths \(FPATH=\{fpath_{1},fpath_{2},\ldots\}\) is considered. An \(fpath\in FPATH\) is a subset of routing processes \(Rp=\{rp_{k},rp_{k+1},rp_{k+2},\ldots,rp_{k+n}\}\) between an \(rp_{src}\) source and an \(rp_{dst}\) destination, where \(rp_{i},rp_{j}\in P_{rp}\) and \(Rp\subset P_{rp}\). Furthermore, we take into consideration the bijection \(f_{fpath}:FPATH\mapsto MATCH\), that is each \(fpath\) corresponds to a \(match\in MATCH\) denoted by \(fpath\triangleq match\). * Events: As mentioned in Section 5.1, there are two types of events: internal and external ones. We note that the internal events are not relevant to the rest of the paper. However, we define them for the completeness of the formal specification. The set of finite internal events \(E_{internal}\) is the following:
* \(PrM(rp_{i},t_{i},m,cp)\) denotes that at \(t_{i}\), an \(rp_{i}\in P_{rp}\) processes a message \(m\in M\) sent by the \(cp\). * \(PrP(rp_{i},t_{i},pkt,rp_{j})\) denotes that at \(t_{i}\), an \(rp_{i}\in P_{rp}\) processes a data packet \(pkt\in PKT\) forwarded by an \(rp_{j}\in P_{rp}\) (\(rp_{i}\
eq rp_{j}\)). The external events considered are the send, the receive, and the delivery events. The set of external events is represented as a finite set \(E_{external}=E_{send}\cup E_{receive}\cup E_{delivery}\). The set of send events \(E_{send}\) is the following:
* \(PrM(rp_{i},t_{i},m,cp)\) denotes that at \(t_{i}\), an \(rp_{i}\in P_{rp}\) processes a message \(m\in M\) sent by the \(cp\). * \(PrP(rp_{i},t_{i},pkt,rp_{j})\) denotes that at \(t_{i}\), an \(rp_{i}\in P_{rp}\) processes a data packet \(pkt\in PKT\) forwarded by an \(rp_{j}\in P_{rp}\) process a data packet \(pkt\in PKT\) forwarded by an \(rp_{j}\in P
\(SdM(m)\) denotes that the \(cp\) sends a message \(m\in M\) to an \(rp_{j}\in P_{rp}\). * \(FwdP(pkt)\): denotes that an \(rp_{i}\in P_{rp}\) forwards a data packet \(pkt\in PKT\) to an \(rp_{j}\in P_{rp}\) (\(rp_{i}\
eq rp_{j}\)). \(E_{receive}\) is composed of one event: * \(RecMP(mp)\): denotes that an \(rp_{j}\in P_{rp}\) receives a message or a data packet \(mp\in MP\). Such an event only notifies the reception of an \(mp\) by \(rp_{j}\). Furthermore, \(E_{delivery}\) is composed of a unique event: * \(DlvMP(mp)\): denotes that an \(rp_{j}\in P_{rp}\) delivered a message or a data packet \(mp\in MP\). A delivery event identifies the execution performed or the consumption of an ingoing \(mp\) by \(rp_{j}\). The set of events associated with \(MP\) is the following: \[E(MP)=\{SdM(m),FwdP(pkt)\}\cup\{RecMP(mp)\}\cup\{DlvMP(mp)\}\] (1) The whole set of events in the system is the finite set: \[E=E_{internal}\cup E(MP)\] (2) The order of occurrence of events can be collected based on the causal dependencies between them. The representation \(\hat{E}\) expresses the causality between events \(E\) in \(P\), using the happened-before relation \((\rightarrow)\) (see Definition 1) where: \[\hat{E}=\{E,\rightarrow\}.\] (3)