Formal Methods for Network Performance Analysis
summary
Formal analysis encodes queues and timed packet sequences in logic, uses Z3 and syntax-guided synthesis to produce concise constraint-based workloads (not single traces), and ships as the fperf prototype. Model sizes reach tens of thousands of variables and constraints; the search runs a few hundred rounds taking a couple hundred seconds and yields workloads in minutes, while verification of a candidate completes in under a second. Evaluations cover packet schedulers and a small leaf-spine network and show exponential scaling, so modular analysis is required.
AI-written summary · about
chapters (10)
- 0:00Intro
- 1:22Existing work focuses on functional correctness
- 3:42Our model: Composition of "queuing modules"
- 5:21Specifying performance properties of interest
- 7:26A single trace is not an informative output
- 9:35Alternative? Conditions on the input
- 10:43Synthesizing workloads
- 11:35Formal Performance Analyzer
- 12:04Case study - Packet scheduling
- 13:43Case study - A (small) leaf-spine network
related talks
26mPerformance Contracts for Software Network Functions
17mPerformance Interfaces for Network Functions
16mA Layered Formal Methods Approach to Answering Queue-related Queries
01h 01mNetwork Verification: Past, Present, and Future
16mAutomatic Parallelization of Software Network Functions
16mSequence Abstractions for Flexible, Line-Rate Network Monitoring
12mMetha: Network Verifiers Need To Be Correct Too!
25mFormal Verification of a Software Defined Delay-Tolerant Network