Zanolin, L and Mascolo, C and Emmerich, W (2002) Model checking programmable router configurations. (Research Note 02/23 ). UCL CS
![[img]](/style/images/fileicons/application_pdf.png)
| 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 itemArchive Staff Only: edit this record