End-to-end Verification of QoS Policies
The 13th IEEE/IFIP Network Operations and Management Symposium (NOMS 2012)
Adel El-Atawy, Taghrid Samak
Conﬁguring 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, trafﬁc ﬂows are assigned speciﬁc classes of service, and service level agreements (SLA) are enforced at routers within each domain. We present a model for QoS conﬁgurations that facilitates efﬁcient property-based veriﬁcation. Network conﬁguration is given as a set of policies governing each device. The model efﬁciently checks the required properties against the current conﬁguration using computation tree logic (CTL) model checking. By symbolically modeling possible decision paths for different ﬂows from source to destination, properties can be checked at each hop, and assessments can be made on how closely conﬁgurations adhere to the speciﬁed agreement. The model also covers conﬁguration debugging given a speciﬁc QoS violation. Efﬁciency and scalability of the model are analyzed for policy per-hop behavior (PHB) parameters over large network conﬁgurations.