High Level Abstraction Modeling for Network Configuration Validation

This paper presents our design and implementation of a Configuration Validation System (ConfVS) which uses a high-level language to help system operators verify network configurations based on formal requirements. In contrast to many existing solutions, ConfVS uses a comprehensive model to formalize the network specification and utilizes the NETCONF protocol to collect configuration data from network devices. In addition, ConfVS uses binary decision diagrams to model the behavior of network devices and provides a prototype to query the device configuration. Requirements and specifications are written in the Erlang language, a general-purpose concurrent programming language. To validate ConfVS, we present a case study to show the features and the expressiveness of ConfVS by performing different types of reasoning with network requirements.