IntentP4: Bridging P4 Temporal Specifications and Executable Network Tests

Abstract

Stateful P4 network functions introduce operational failures that emerge only under temporally ordered packet sequences and control-plane states. Existing temporal verifiers (e.g., P4TV) stop at logical verdicts, while dynamic testers (P4Testgen, CHIMERA) execute packets without temporal specifications, and both require operators to hand-author formal specifications. We present IntentP4, a formal-methods-aided pipeline that closes this loop: it translates an operator's natural-language intent into a P4LTL specification and then into a replayable multi-packet test case (packet sequence, control-plane rules, external operations, oracles), grounded throughout in compiler artifacts via a tool-queryable ProgramContext and gated by deterministic per-stage validators. On five stateful P4 programs spanning access control, monitoring, heavy-hitter detection, failure recovery, and load balancing, the P4LTL-to-test generator produces 10 scenarios, 89 packets, and 110 unified execution operations that pass eight consistency checks; on 11 specification subtasks, 4 strictly pass and 3 are semantically close; and an integrated BMv2/Mininet loop exposes runtime failures including a firewall policy-bypass manifestation and a missing multi-table control-plane entry under controller convergence.