Testing OpenFlow interaction property based on hierarchy CPN

OpenFlow is a new protocol which enables researchers to run experimental protocols in a network without changing the network topology. In the paper, we analyze and test OpenFlow based on a formal method, such as CPN (colored Petri net). To avoid state exploration, we mainly focus on testing the interaction property of OpenFlow. According to the latest OpenFlow specification, we construct its hierarchy CPN model and analyze the model with CPN tools. We propose two methods to generate the test sequences covering the interaction property. We also design an algorithm to generate the test sequences automatically. The related experiments are carefully designed and executed in four kinds of network environment, respectively.