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.
CITATION STYLE
Zanolin, L., Mascolo, C., & Emmerich, W. (2010). Model checking programmable router configurations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5765 LNCS, pp. 473–491). https://doi.org/10.1007/978-3-642-17322-6_20
Mendeley helps you to discover research relevant for your work.