Skip to content
Log in
Book Open access

IntentP4: Bridging P4 Temporal Specifications and Executable Network Tests

Ruonan Feng Mingming Zhang Yu Jiang Shijie Gao Yaping Liu Shuo Zhang
Aug 2026 · Proceedings of the ACM SIGCOMM 2026 Conference · 0 citations · 20 references

TL;DR

IntentP4 is presented, a formal-methods-aided pipeline that translates an operator's natural-language intent into a P4LTL specification and then into a replayable multi-packet test case, grounded throughout in compiler artifacts via a tool-queryable ProgramContext and gated by deterministic per-stage validators.

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.

DOI Semantic Scholar
Read PDF

Similar papers

QiMeng-VPID: Verification-Grounded Port-Level Iterative Decomposition for Complex Verilog Generation

This work proposes VPID, a multi-agent framework for generating complex Verilog that achieves monotonic functional improvement and introduces an experience-guided refinement strategy that distills historical waveform mismatches into constraints, guiding the targeted debugging for the unverified ports.

Hongguang Wang, Jiaming Guo, Rui Zhang et al. · 0 citations
Preprint Jul 2026

PULSE: An Executable Contract Language for Spatiotemporal Knowledge Graph Engineering

This work presents PULSE, an Object-Process-Methodology-inspired language that localizes four operational roles and their write effects in one typed runtime, here, modes denote operational roles rather than modal or deontic logic.

Dongxu Yang, Ziyi Liang · 0 citations
Preprint Jul 2026

ContainmentBench: Trace-Based Evaluation of Post-Exposure Containment in Tool-Using LLM Agents

ContainmentBench, a sandboxed benchmark comprising a 504-scenario specification dataset, a shared rollout-trace schema, and stage-scoped metrics for endpoint violations, logged propagation, and explicitly authorized taint-exposed proposals that commit, is introduced.

Wenhao Lan, Shan Li, Meiqi Wu et al. · 0 citations
Preprint Jul 2026

Compile, Then Page: Executable SOP Programs and a Capability-Gated Runtime for Procedural LLM Agents

Enterprise agents must follow long-horizon, conditional, safety-critical standard operating procedures (SOPs), which are compiled into executable pseudo-code and run with a program-guided stack machine that pages the active frame while an LLM performs semantic execution.

Chenglin Yu, Lichao Yin, Qingxin Fan et al. · 1 citation
Preprint Jul 2026

From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs

A Petri-net-guided methodology for test generation over concurrent stateful Rust APIs that represents API resources, lifecycle conditions, and causal dependencies as colored tokens and transitions; derives legal deep-state, near-legal, and partial-order concurrent scenarios; and uses them as a constrained intermediate representation for LLM-based code synthesis.

Kaiwen Zhang, Guanjun Liu · 0 citations
Open access Aug 2026

RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation

RunbookFX is presented, a typed functional domain-specific language that elevates incident response from natural-language suggestions to executable programs whose safety is established statically, and key insight is that incident-response safety decomposes into three interacting dimensions: risk severity, exercised capabilities, and rollback resource availability.

Yifan Xiao, Shijie Li, Yuhao Ge · 0 citations