CUED Publications database

Model checking programmable router configurations

Zanolin, L and Mascolo, C and Emmerich, W (2010) Model checking programmable router configurations. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 5765 L. pp. 473-491. ISSN 0302-9743

Full text not available from this repository.


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.

Item Type: Article
Depositing User: Cron Job
Date Deposited: 17 Jul 2017 19:26
Last Modified: 30 Mar 2021 06:42
DOI: 10.1007/978-3-642-17322-6_20