End-to-end Verification of QoS Policies
Venue
The 13th IEEE/IFIP Network Operations and Management Symposium (NOMS 2012)
Publication Year
2012
Authors
Adel El-Atawy, Taghrid Samak
BibTeX
Abstract
Configuring a large number of routers and network devices to achieve quality of
service (QoS) goals is a challenging task. In a differentiated services (DiffServ)
environment, traffic flows are assigned specific classes of service, and service level
agreements (SLA) are enforced at routers within each domain. We present a model for
QoS configurations that facilitates efficient property-based verification. Network
configuration is given as a set of policies governing each device. The model
efficiently checks the required properties against the current configuration using
computation tree logic (CTL) model checking. By symbolically modeling possible
decision paths for different flows from source to destination, properties can be
checked at each hop, and assessments can be made on how closely configurations
adhere to the specified agreement. The model also covers configuration debugging
given a specific QoS violation. Efficiency and scalability of the model are analyzed
for policy per-hop behavior (PHB) parameters over large network configurations.
