Formal Analysis of Passive Measurement Inference Techniques

Abstract— Verifying the accuracy of a passive measurementsbased inference technique under all possible network scenarios is a difficult challenge - the measurement point has limited observability of events along the path, and monitored paths can exhibit a wide range of network properties (packet loss, reordering, end-end delay, route changes). In this paper, we propose and apply formal verification techniques to exhaustively verify the correctness of an inference technique. We apply this approach to the problem of inferring packet retransmissions and reorderings from passively observed packets at a single measurement point. We define classification rules for this inference problem and, through a combination of model-checking and formal reasoning, uncover all possible events in the network for which the rules produce incorrect inferences. Our work is novel in its use of formal verification tools for evaluating inference techniques in network measurements.

• Type: Conference
• Year: 2006
• Where: INFOCOM
• Authors: Sharad Jaiswal, Gianluca Iannaccone, James F. Kurose, Donald F. Towsley
• Keywords: Communications, Inference Techniques, INFOCOM 2006, Measurement Point, Passive Measurementsbased Inference