Network Simulator-centric Compositional Testing
Tom Rousseaux, Christophe Crochet, John Aoga, Axel Legay
TL;DR
NSCT addresses the challenge of verifying time-varying network properties in protocol testing by extending MBT with a network-simulator circle that includes Ivy specifications and the Shadow simulator. By coupling time-aware Ivy modeling with a time- and event-driven NS, NSCT achieves reproducible, deterministic testing of real protocol implementations, validated through a QUIC (picoquic) case study that exposed and fixed a time-varying compliance issue. The work introduces a PFV toolchain integrating Ivy, Shadow, and containerized workflows to monitor time-varying properties and enables online debugging of implementations. It demonstrates how time-breakpoint techniques and network-condition variation yield actionable insights and higher fidelity verification, with potential extensions to broader QUIC variants and MPQUIC scenarios, supported by a dedicated artefact repository.
Abstract
This article introduces a novel methodology, Network Simulator-centric Compositional Testing (NSCT), to enhance the verification of network protocols with a particular focus on time-varying network properties. NSCT follows a Model-Based Testing (MBT) approach. These approaches usually struggle to test and represent time-varying network properties. NSCT also aims to achieve more accurate and reproducible protocol testing. It is implemented using the Ivy tool and the Shadow network simulator. This enables online debugging of real protocol implementations. A case study on an implementation of QUIC (picoquic) is presented, revealing an error in its compliance with a time-varying specification. This error has subsequently been rectified, highlighting NSCT's effectiveness in uncovering and addressing real-world protocol implementation issues. The article underscores NSCT's potential in advancing protocol testing methodologies, offering a notable contribution to the field of network protocol verification.