Model Checking the OpenFlow Protocol Using SPIN

Software-Defined Networking (SDN) is a new architecture of separation of logical control and data forwarding. Although this separation has brought many benefits to the network, it also exposes the network to more risks. OpenFlow protocol is a communication protocol between them. The correct behavior of OpenFlow protocol is critical to SDN. Model checking technology has been widely applied to the protocol verification. This paper presents the process of model checking the OpenFlow protocol using SPIN. First, we describe an abstract formal model of OpenFlow protocol. And then we translate the model with PROMELA which is a model description language. Finally we apply the model checker (SPIN) to verify properties. In the process, it is realized that to pay more attention to the delay of SDN is more efficient when updating OpenFlow protocol version.