 state management. Thus, we could use program analysis to refactor the code and identify the minimum set of statements that capture such forwarding logic. For example, in Figure 3.6, the bold and bold italics lines are a (dynamic) program slice where the load balancer relays the first packet of a flow. This small code snippet captures the forwarding behavior of this NF. Identifying this snippet automatically from the original code would improve the efficiency of manual analysis and automatic verification. Refactoring the logic in an NF program could benefit NF veri- fication in many ways. For example, finding out the state update logic helps to build a finite state machine (FSM) of that box; in the network-wide, assembling FSMs of multiple NFs can help to find out the network-wide invariant violation. In addition, refactoring NF logic helps to minimize the number of statements that would lead to a certain behavior (e.g., packet corruption, unexpected drop), and this minimization not only eases manually program analysis but also speeds up other automated program analysis solutions (e.g., symbolic execution). 3.5.1.3 Models Referring to various existing NF models [54-56,65-67] and the cur- rent hardware programmability [68-70], we adopt an OpenFlow-like model with a stateful data plane extension. The abstract model is expressed as tables in Figure 3.7, and each table describes the packet processing logic under a certain configuration (e.g., C1 in the figure). 3 Network Function Virtualization Match Action Figure 3.7 Model. State State Configuration = C1 S1AP(f1,S1) Fwd(f1,S1) Upd(f1,S1) Configuration = 6 S2AP(f2,S2) Fwd(f2,S2) Upd(f2,S2) Each entry in the table represents certain processing logic and consists of match and action fields. As a stateful data plane, the match/action fields operate on both flows and state variables. The match is executed on flows and states, and the action not only forwards packets (with possible transformation) but also triggers state transition. In table C1 in Figure 3.7, if an incomi