oundation to apply SFC-Checker. In this section, we use examples of IDS and load balancer to illustrate the modeling process. It induces NF programs [76, 77] to the abstract models in Figure 3.8. An IDS is configured with a list of denied flows "DENY," and flows not in this list are allowed by default. An IDS has no output-impacting states. A load balancer in round-robin mode forwards new flows to one of the backend servers pointed by an internal state "index." And the index increased circularly for each new flow. To generate a DFA, one needs to decide the state space and the state transition. Each entry in the model can express a state transition as follows. fwd(f,s) transit(f,s) The packet processing logic takes f as input and outputs forward(f,s) and the states transit from S to transit(f,s). However, the state space needs to be in proper granularity. Too fine a granularity would cause a state space explosion. For example, a cache can have 2cache_size possible values, which is not practical to verify. While too coarse a granularity cannot guarantee the correctness or efficiency of verification. For example, the state "idx=*" in load balancer can be used to represent any states but is not useful to identify the exact next hops. Therefore, we propose to refine each entry to the granularity of possible next hops. For example, if the load balancer has two backend 3.6 VNF Placement servers configured, then the state-matching field is refined to two states "idx=0" and "idx=1" to indicate two possible next hops. Thus, we can transform the model to DFAs (as is shown in Figure 3.8). Next, we can leverage SFC-Checker [55] to check the end-to-end reachability, and the result is shown in the evaluation section. Model-based NF programming is the reverse process of model generation. To generate an NF program from a match action table, the program first contains a loop starting with packet input function. Each row in the match action table is transformed to a branch in the program. The branch has the conjunction (AND) of the