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.

Analysis of concurrent systems, such as computer/communication networks and manufacturing systems, usually employs formal discrete event models. The analysis then includes model validation, property verification, and performance evaluation of such models. The DEVS (Discrete Event Systems Specification) formalism is a well-known formal modeling framework which supports specification of discrete event models in a hierarchical, modular manner. While validation and verification using formal models may not resort to discrete event simulation, accurate performance evaluation must employ discrete event simulation of formal models. Since formal models, such as DEVS models, explicitly represent communication semantics between component models, their simulation cost is much higher than using simulation languages with informal models. This paper proposes a method for simulation speedup in performance evaluation of concurrent systems using DEVS models. The method is viewed as a compiled simulation technique which eliminates run-time interpretation of communication paths between component models. The elimination has been done by a behavior-preserved transformation method, called model composition, which is based on the closed under coupling property in DEVS theory. Experimental results show that the simulation speed of transformed DEVS models is about 14 times faster than original ones.

Despite their attractive properties, networked virtual environments (net-VEs) are notoriously difficult to design, implement and test due to the concurrency, real-time and networking features in these systems. The current practice for net-VE design is basically trial and error, empirical, and totally lacks formal methods. This paper proposes to apply a Petri net formal modeling technique to a net-VE: NICE (Narrative Immersive Constructionist/Collaborative Environment), predict the net-VE performance based on simulation, and improve the net-VE performance. NICE is essentially a network of collaborative virtual reality systems called CAVE-(CAVE Automatic Virtual Environment). First, we present extended fuzzy-timing Petri net models of both CAVE and NICE. Then, by using these models and Design/CPN as the simulation tool, we have conducted various simulations to study real-time behavior, network effects and performance (latencies and jitters) of NICE. Our simulation results are consistent with experimental data.