Sla-Verifier: Stateful And Quantitative Verification For Service Chaining

Network verification has been recently proposed to detect network misconfigurations. Existing work focuses on the reachability. This paper proposes a framework that verifies the Service Level Agreement (SLA) compliance of the network using static verification. This work proposes a quantitative model and a set of algorithms for verifying performance properties of a network with switches and middleboxes, i.e., service chains. We develop SLA-Verifier and evaluate its efficiency using simulation on real-world data and testbed experiments. To improve the SLA violation detection accuracy, our system uses verification results to optimize online monitoring.