UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Model checking programmable router configurations

Zanolin, L; Mascolo, C; Emmerich, W; (2002) Model checking programmable router configurations. (Research Note 02/23 ). UCL CS Green open access

[img]
Preview
PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
235Kb

Abstract

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.

Type:Report
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 > Computer Science

View download statistics for this item

Archive Staff Only: edit this record