Model Checking Programmable Router Configurations

Programmable networks offer the ability to customize router behaviour at run time, thus providing new levels of flexibility for network administrators. We have developed a programmable network framework and used it to implement Differentiated Services (DiffServ) in order to guarantee network quality of service. Part of the framework is an application-specific language that we use to program router configurations. The ability to change these configurations dynamically introduces the danger of router misbehaviour. We show an approach that uses model checking techniques to analyze router configurations prior to their deployment in a router. Our approach allows network administrators to specify correctness criteria and check whether or not specific router configurations meet these criteria.

• Type: Conference
• Year: 2010
• Where: BIRTHDAY
• Authors: Luca Zanolin, Cecilia Mascolo, Wolfgang Emmerich
• Keywords: Applied Computing, BIRTHDAY 2010, Programmable Network, Router, Router Configurations