 5 SDN and NFV in 5G State Match Action Expert knowledge documentation configuration testing/analysis Figure 5.13 Model used for SFC verification. the forwarding graphs only capture the forwarding behavior of the network but not the state transitions of the NFs. On the one hand, receiving and forwarding a packet may trigger the NF's state transition. On the other hand, the state changes may affect the forwarding behav- ior of subsequent packets of the same flow. Thus, naturally we should combine them in order to correctly verify the stateful network behav- ior. We can use a stateful forwarding graph (SFG) that encodes both the state transitions and forwarding behavior. We develop an algo- rithm that automatically generates the SFG from our NF tables and FSMs. Figure 5.14 shows an example for the SFG. In an SFG, each node is denoted as (H, ,D,S), representing any packet in the packet header space H arriving at a network device (switch or NF) D, when the net- work device is in a particular state S. H1, SW1 H1, SWO TCPEstablish TCPEstablish H1, FW NEW/WAIT NEW/WAIT Timeout Timeout H4, SW2 H1, SW2 "Active" "Inactive" state state Figure 5.14 Stateful forwarding graph for SFC verification. 5.3 Core Network Functions Virtualization: vEPC An edge pointing from one node (H1, D1, S1> to another (H2, D2, S2> means when a packet in H arrives at D1 with state S1, it will be modified to H2 and forwarded to a device D2 at state S2. If the device D1 does not modify the packet header, then H is equal to H2. If the packet H1 does not trigger the state transition, then S1 is equal to S2. Figure 5.14 shows an example of a path of packets H traversing through D0, D1, and D2. Essentially, an SFG edge can represent one of two events: (1) a packet is modified and forwarded to next hop or dropped; (2) a device is changing its state to the next state. Accordingly, we use two different types of edges to represent the different events. Using the SFG, we develop a verification algorithm that is capable of verifying the dynamic and stateful b