zr [53] proposes an approach to identify state variable in NF programs. It basically uses some NF-specific features (e.g., program structure, packet libraries), and leverages program slicing techniques to find out state variables. This work provides an approach to analyze NFs but does not go further in NF modeling. Manually generated models: A set of works view NFs as deter- ministic finite automata (DFA). For example, BUZZ [54] uses DFA to represent each NF in the network, finds possible violation 3 Network Function Virtualization states in each DFA, and use a network-wide model to generate traces (that may trigger the violation) for testing. In another example, SFC-Checker [55] also views NFs as DFAs; it mainly answers a question, given a network with NFs and a series of packet traces, whether there is a risk of violations (unexpected reachability/unreachability). The DFAs in these works are manually generated and directly used to replace the NFs, which implies possible incompleteness. Modeling language design: SymNet [56] proposes a symbolic execution-friendly language to remove these two features for NF programming. Both works aim to develop NF programs that can be symbolic executed SO that program bugs can be found out early during the development. These two approaches provide new ways to model NFs but still require programmers to writing NF programs. 3.5.1 Source-Code-Based Modeling One way to perform modeling is to leverage recent advances in code analysis techniques. Wu et al. [57] analyzes the source code of a given network function to automatically generate an abstract packet forwarding model. It is built on top of the following code analysis methods. 3.5.1.1 Background Program slicing A program slice is a minimum set of statements in a given program that lead to certain behaviors. The behavior is expressed as the values of variables in a certain statement. Program slicing has been shown to be useful for program debugging, parallelization, and integration [58]. The basic methodology to get a program sli