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

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.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as JSONCSVXML

Downloads by country - last 12 months

Export as JSONXMLCSV

Archive Staff Only

View Item