SDN (Software-Defined Networking) enables software applications to program individual network devices dynamically and therefore control the behavior of the network as a whole. Incomplete programming and/or inconsistency with the network policy of SDN software applications may lead to verification issues. The objective of this paper is to describe the formal modeling that uses the process algebra called pACSR and then suggest a method to verify the firewall application running on top of the SDN controller. The firewall rules are translated into a pACSR process which acts as the specification, and packet's behaviors in SDN are also translated to a pACSR process which is a role as the implementation. Then we prove the correctness by checking whether the parallel composition of two pACSR processes is deadlock-free. Moreover, in the case of network topology changes, our verification can be directly applied to check whether any mismatches or inconsistencies will occur.

Even though various kinds of IPv6 transition mechanisms have been developed for the transition to an IPv6 network, these transition mechanisms take no stance on whether applications support IPv6 or not. This paper describes why the transition period between IPv4 and IPv6 applications may not be straightforward and applications should be ported to support both IPv4 and IPv6; such applications are called "IP version-independent applications." Also, this paper examines and empirically evaluates overhead of the IP version-independent applications, since the performance implication is not well known. The overhead might be very dependent on data sizes and network performance, but it was relatively minimized for general Internet traffic with larger data sizes and lower network latency.

Due to the cost of multicast state management, multicast address allocation, inter-domain multicast routing of traditional IP multicast scheme, ASM leads to a search for other multicast schemes. This paper presents a new solution to the problems mentioned above based on IPv6. The proposed scheme provides an enhanced scheme supporting the strengths of SSM in basic Xcast. This is achieved by adding MLDv2 operations at recipient's side and a new control plane into existing Xcast. The proposed scheme does not only provide the transparency of traditional multicast schemes to sources and recipients, but it also enhances the routing efficiency in networks. Intermediate routers do not have to maintain multicast state, so that it results in a more efficient and scalable mechanism to deliver native multicast datagrams. Also, the seamless integration in Mobile IPv6 can support multicast efficiently for mobile nodes in IPv6 networks by avoiding tunnel avalanches and tunnel convergence. We've attempted to prove this alternative architecture by both simulation and implementation, respectively. Our approach cannot fundamentally perform for many large groups distributed widely as effectively as traditional multicast schemes. However, we believe that the resulting scheme is simple, efficient, robust, transparent, and to the extent possible, scalable in case that recipients are clustered in subnets.

NAT-PT and DSTM are becoming more widespread as de-facto standards for IPv6 dominant network deployment. But few researchers have empirically evaluated their performance aspects. In this paper, we compared the performance of NAT-PT and DSTM with IPv4-only and IPv6-only networks on user applications using metrics such as throughput, CPU utilization, round-trip time, and connect/request/response transaction rate.