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


Download (241kB)


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
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/784
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item