## 5 System Model
### SDN Model  
We developed the SDN model by adapting the sets \(P\), \(M\) (also extended to the set \(MP\)), and \(E\), presented in the distributed system model of Section 5.1, to the SDN context and by adding the sets \(MATCH\), \(MP\), \(PFLOW\), and \(FPATH\), which correspond, respectively, to the set of matches, the set of messages and data packets, the set of packet flows, and the set of forwarding paths, which are specific to the SDN model. * Processes: The system under consideration is composed of a set of processes \(P=\{p_{1},p_{2},\ldots\}\mid P=P_{cp}\cup P_{rp}\) where \(P_{cp}=\{cp\}\) represents the controller process \(cp\) and \(P_{rp}=\{rp_{1},rp_{2},\ldots\}\) represents the set of routing processes of OpenFlow switches. * Matches: We consider a finite set of matches \(MATCH=\{match_{1},match_{2},\ldots\}\). A match \(match\in\ MATCH\) is a field value that identifies a forwarding path in the network. It is important to mention that the match is a key attribute in establishing the proposed updating algorithm (see Section 7.2). In fact, each update is performed based on a match. This is because an update makes reference to a forwarding path \(fpath_{\mu}\in FPATH\), a packet flow \(pflow_{\tau}\in PFLOW\), which is taking route to its destination according to \(fpath_{\mu}\), and to any OpenFlow message \(m\in M\) disseminated by the controller to update any routing process \(rp\in fpath_{\mu}\) that shares the same match \(match_{\lambda}\in MATCH\). * Messages and data packets: The system includes a set of messages and data packets \(MP=\{mp_{1},mp_{2},\ldots\}\mid MP=M\cup PKT\) where \(M=\{m_{1},m_{2},\ldots\}\) represents the OpenFlow messages and \(PKT=\{pkt_{1},pkt_{2},\ldots\}\) represents the data packets. In addition to the set of messages \(M\), we consider the set of OpenFlow message types \(M_{type}\)[2] where \(f_{message}:M\mapsto M_{type}\). Furthermore, we note that each message \(m\in M\) corresponds to a \(match\in MATCH\), denoted by \(m\triangleq match\). Furthermore, a \(match\) may also correspond to a subset of OpenFlow messages. We denote a message \(m\in M\) as \(m=(cp,t_{cp},OpenFlow_{\_message},rp_{j})\) where a controller \(cp\) sends an \(OpenFlow_{\_}message\) to a \(rp_{j}\in P_{rp}\) at \(t_{cp}\) (the logical clock of \(cp\)). Note that the tuple \((cp,t_{cp})\) represents the identifier of a message \(m\in M\). In this paper, we consider controller-to-switch messages, and in particular the \(FlowMod\) message. This message allows the controller to modify the state of OpenFlow switches either by adding, modifying, or deleting entries. The \(FlowMod\) message is composed of various structures (see the details in [2]). In this work, we consider \(match\) and \(command\) as the relevant \(FlowMod\) message structures. In fact, the former specifies to which packet flow an entry corresponds, whereas the latter specifies the action to be performed on the matched packet flow. We consider \(FlowMod\) as a relevant message, where \(command\) and \(match\) represent the \"\(OpenFlow_{\_}message\)\" structure in the specification of a message \(m\in M\). A packet \(pkt\) in the subset \(PKT\) mentioned above is denoted as \(pkt=(rp_{i},t_{i},header,data,rp_{j})\), where an \(rp_{i}\) forwards at the logical clock \(t_{i}\) a data packet, composed of a \(header\) and \(data\), to an \(rp_{j}\) such that \(rp_{i},rp_{j}\in P_{rp}\) and \((rp_{i}\
eq rp_{j})\). Note that the tuple \((rp_{i},t_{i})\) represents the identifier of a data packet \(pkt_{i}\in PKT\). The header of each data packet piggybacks a \(match\in MATCH\) that corresponds to all \(match\) of packets belonging to the same packet flow. The data consist of the payload (the current intended message). * Packet flow: We consider a finite set of packet flows \(PFLOW=\{pflow_{1},pflow_{2},\ldots\}\). A \(pflow\in PFLOW\) (also \(pflow\subset PKT\)) is a sequence of packets between a source \(rp_{i}\) and a destination \(rp_{j}\), \((rp_{i},rp_{j}\in P_{rp})\).