Modeling and verifying the topology discovery mechanism of OpenFlow controllers in software-defined networks using process algebra.