Model Checking Programmable Router Configurations with Spin

Luca Zanolin

Dip di Elettronica ed Informazione
Politecnico di Milano
Piazza Leonardo da Vinci
20100 Milano, Italy

Cecilia Mascolo and Wolfgang Emmerich

Dept. of Computer Science
University College London
Gower Street, London WC1E 6BT, UK

Programmable networks offer the ability to customize router behaviour at run time, thus increasing exibility of network administration. Programmable network routers are configured using domain-specific languages. The ability to evolve router programs dynamically creates potential for misconfigurations. By exploiting domain-specific abstractions, we are able to translate router configurations into Promela and validate them using the Spin model checker, thus providing reasoning support for our domain-specific language. To evaluate our approach we use our configuration language to express the IETF's Differentiated Services specification and show that industrial-sized DiffServ router configurations can be validated using Spin on a standard PC.

[ Home ] [ Profile ] [ Research ] [ Selected Publications ]

Updated on: 31/12/2002
Wolfgang Emmerich