With the evolution of modern networks, network operators are able to flexibly deploy Service Function Chains (SFCs) in accordance with network policy requirements to achieve desired purposes. At the same time, to reduce the latency of processing packets through SFCs, an increasing number of network operators are designing SFCs to operate in parallel. In addition, many service functions are designed to be stateful, making the processing behavior of packets state-dependent, but the state is complex and arbitrary, which introduces greater complexity and uncertainty and makes the verification of SFCs behavior more difficult. To verify the correctness of stateful parallel SFCs, a formal verification method named SPV is proposed in this paper. SPV first defines the correctness attribute of stateful parallel SFCs, and then uses Coloured Petri Nets (CPN) for offline modeling of stateful parallel SFCs. This model describes the topological structure and behavior of the stateful parallel SFCs and enhances the expressiveness of the CPN model with Standard ML Language (ML) functions. In experiments, by analyzing the reachability graph and state space of the stateful parallel SFC's CPN model, the correctness attribute of the stateful parallel SFCs are verified, completing the correctness verification of stateful parallel SFCs. Moreover, these results also demonstrate the potential of CPN-based modeling for the verification of SFCs in stateful networks.

Network Function Virtualization (NFV) virtualizes traditional hardware-based Network devices and intermediate boxes into Virtual Network Functions(VNF). A series of VNF through which packets pass constitute a Service Function Chain(SFC). VNF can be placed as software on general-purpose commercial servers, greatly increasing the flexibility of network services and reducing costs. Packets need to pass through many VNFs to get from the source to the destination of an SFC. To reduce end-to-end delay caused by virtualization and chain length. SFC parallelization has been a successful solution. However, the existing Parallelized SFC(PSFC) placement method does not conform to the distributed design idea of network services. In this paper, we propose a distributed delay-aware PSFC placement approach called DPSFC that all VNF in PSFC are placed on different physical nodes as much as possible and balancing link propagation delay and VNF processing delay to reduce packet deposition at the merge node of parallel modules(pm). Finally, a link packet marking method is proposed to reduce the extra link bandwidth of distributed VNF placement. The simulation results show that compared with the existing approaches, our approach can improve the request acceptance ratio of PSFC while ensuring end-to-end delay.

To efficiently meet the flexible service requests in Cloud Computing Data Centers (CloudCDC), the integrated construction of Service Function Chaining (SFC) and business system is researched based on Colored Petri Net (CPN). The general composition of multiple Service Functions (SFs) is studied at first. After analyzing the possible conflicts among the SFs that compose SFC, a novel method of SFC construction is proposed. Besides, to prove the correctness of the SFC construction, a method for verifying the constructed SFC before deployment is designed which composes the CPN model of object-oriented technology to observe the local behavior and global interaction of SFC respectively.

The service requirements from the customer are getting more and more complicated, and the users' demands for continuous uptime availability guaranteed in SLA become more and more strict. Under such circumstances, Service Function Chaining (SFC) requires more flexibility and scalability. Therefore researchers and developers have proposed plenty of complex structured solutions for the provisioning of SFC in the network. In this paper, to specify and configure these complex structured SFC, the concept of Path Adjustable SFC (P A-SFC) is proposed. After analyzing its possible traffic steering, two forwarding modes - load balancing mode and parallel mode are designed. Then the PA-SFC is modeled using YANG data modeling language. With the proposed approach, the SFC can be adjusted into a parallel chain or multiple loads balancing chains automatically under the control of the SDN controller.