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
Abstract:
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.
 |
Updated on: 31/12/2002
|
|