Title:	TOWARDS VERIFYING NETWORK TIMELINESS
Author(s):	Soudeh Ghorbani
ISBN:	978-989-8704-46-7
Editors:	Piet Kommers, Tomayess Issa, Adriana Backx Noronha Viana, Theodora Issa and Pedro Isaías
Year:	2022
Edition:	Single
Keywords:	Real-Time Properties, Networks, Verification, Tests
Type:	Reflection Paper
First Page:	201
Last Page:	204
Language:	English
Cover:
Full Contents:	click to dowload
Paper Abstract:	Today's networks should meet strict real-time requirements. The reliability of emerging computing use cases such as autonomous vehicles, IoT, and cloud-based systems, for example, hinges on the ability of the network to deliver information to devices in the right time frame. Formal reasoning about the timeliness of networks is challenging. Despite significant progress towards building various network verification frameworks, e.g., via applying model checking (exhaustive exploration of an abstract mathematical model of the network), the scale of networks and classes of properties that can be formally verified remain limited. Crucially, the existing network models abstract away the notion of time (essential for verifying real-time properties) and focus instead on a narrower set of logical properties. Real-time properties are strictly stronger—and computationally more expensive—to verify because the events that affect them (such as congestion) can change rapidly and require more refined models of the network. Larger models, in turn, increase the complexity of formal model verification techniques. In practice, to sidestep the scalability and expressiveness limitations of formal verification, testing is used extensively to check some basic properties (such as reachability) of large-scale networks. Despite its great scalability, testing has well-known shortcomings including low coverage of state space and the postmortem detection of major violations. It is, therefore, not surprising that sweeping network failures and violations of critical invariants regularly transpire despite various testing and monitoring systems being "always-on". Availability and maintaining service level objectives (SLOs)— contingent on meeting real-time requirements—continue to be the biggest challenges facing operators today. We argue that verifying real-time properties of critical networks requires the strengths of both approaches: it requires the coverage of verification techniques such as model checking as well as the speed and scalability of testing. This paper outlines the desired properties for such a hybrid technique and the challenges for achieving them.
	Go Back