UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Model checking programmable router configurations

Zanolin, L; Mascolo, C; Emmerich, W; (2010) Model checking programmable router configurations. Green open access

[img]
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 > 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
Downloads since deposit
371Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item