Model checking programmable router configurations.
Programmable networks offer the ability to customize routerbehaviour at run time, thus increasing flexibility of network administration.Programmable network routers are configured using domain-specificlanguages. The ability to evolve router programs dynamically creates potentialfor misconfigurations. By exploiting domain-specific abstractions,we are able to translate router configurations into Promela and validatethem using the Spin model checker, thus providing reasoning support forour domain-specific language. To evaluate our approach we use our configurationlanguage to express the IETF?s Differentiated Services specificationand show that industrial-sized DiffServ router configurations canbe validated using Spin on a standard PC.
|Title:||Model checking programmable router configurations|
|Open access status:||An open access version is available from UCL Discovery|
|Additional information:||Imported via OAI, 7:29:00 20th Jul 2005|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science
UCL > School of BEAMS > Faculty of Engineering Science > Computer Science
Archive Staff Only