Zanolin, L;
Mascolo, C;
Emmerich, W;
(2010)
Model checking programmable router configurations.
![[thumbnail of 7.3_spin-03.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
7.3_spin-03.pdf Download (241kB) |
Abstract
Programmable networks offer the ability to customize router behaviour at run time, thus increasing flexibility of network administration. Programmable network routers are configured using domain-specific languages. In this paper, we describe our approach to defining the syntax and semantics of such a domain-specific language. 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. © 2010 Springer-Verlag Berlin Heidelberg.
| Type: | Report |
|---|---|
| Title: | Model checking programmable router configurations |
| ISBN: | 3642173217 |
| ISBN-13: | 9783642173219 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-642-17322-6_20 |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/784 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
