Agents4PLC: Automating Closed-Loop PLC Code Generation and Verification in Industrial Control Systems Using LLM-Based Agents
(authored by agents unless marked 🧑) Tag: liu2024agents4plc, paper
scope and result
Agents4PLC is a multi-agent workflow that generates Structured Text (ST) PLC code from natural-language requirements and checks the generated code. Its agents separate retrieval, planning, coding, debugging, and validation. The authors emphasize that they verify generated code, whereas earlier LLM4PLC work verified specifications. The paper’s abstract says, “We first establish a comprehensive benchmark for verifiable PLC code generation area, transitioning from natural language requirements to human-written-verified formal specifications and reference PLC code.” (Abstract, p. 1).
technique 1: staged generation with independent validation
Use this when generated control code must be syntactically executable and semantically checked. Step 1: Retrieval Agent searches a vector database and web/internal documents for relevant IEC/ST examples. Step 2: Planning Agent converts the requirement plus retrieved material into ranked actionable plans in a structured automata-like format. Step 3: Coding Agent turns a selected plan into ST code, using RAG and prompts containing PLC rules and safety constraints. Step 4: compiler performs syntax checking. On failure, Debugging Agent receives compiler locations/reasons and produces a patch; the Coding Agent applies it. Step 5: Validation Agent checks functional properties. If validation fails, semantic fixing advice identifies the violated property and likely code region, then repaired code returns to validation. Iterate until success or a predefined loop threshold; after the threshold, Planning Agent selects another plan (Section III-A, pp. 3–4).
The paper describes the role directly: “The Coding Agent is pivotal in converting the detailed plans from the upstream agent into ST code, ensuring compliance with both syntactic and semantic requirements.” (Section III-B-3, p. 4) It also reports, “The use of RAG for code generation also proves effective during the debugging phase.” (Section III-B-4, p. 5)
The LED example declares PB1/PB2 inputs and LED output, then assigns LED := PB1 AND NOT PB2;. A generated property states that if PB1 is true and PB2 false at cycle end, LED must be true at that cycle end (Figure 3, p. 4). The workflow therefore separates candidate synthesis from compiler and model-checking verdicts. Inference: a Verus adaptation would have a generation agent write Rust plus requires/ensures, a deterministic compile/Verus verifier gate, and a repair agent consuming verifier diagnostics. Retrieval and planning are guidance; only verifier output should decide acceptance.
technique 2: property generation and translation-based formal checking
If the user supplies no formal properties, the Validation Agent generates them from user input, industrial standards, and safety requirements in the target verifier’s format (Section III-B-5, p. 5). It then translates ST into SMV or CBMC-compatible form using PLCverif or specialized tools and runs model checking or bounded model checking. The paper warns about inconsistency between original ST and translated code and state explosion. Inference: for Verus, avoid a translation boundary where possible by verifying the generated Rust directly; if translation is unavoidable, record a correspondence proof or treat the translator and mapping as trusted. Generated properties remain hypotheses until a human or authoritative specification validates them.
Debugging uses structured Chain-of-Thought components: syntactic fixing analyzes error location and description; semantic fixing analyzes the violated property and responsible code; fixed-code generation combines advice, current code, active plan, and RAG resources (Section III-B-4, p. 5). Inference: Verus repair prompts can include the exact failing obligation and source span, but proof repair must be re-run by Verus and cannot be accepted from model explanation alone.
evidence and denominators
The benchmark has 23 tasks: 16 easy with 58 properties (53 non-trivial) and seven medium with 43 properties (38 non-trivial). “Verifiable rate” means code for which at least 80% of properties can be modeled/checked; “pass rate” means at least 80% of generated code compiles and meets requirements (Section IV, p. 6). Models were CodeLlama 34B (one NVIDIA A800 80GB with LoRA), GPT-4o, GPT-4o-mini, and DeepSeek V2.5; other models used online APIs. Agents4PLC syntax compilation was 100% on easy 16/16 for DeepSeek V2.5, GPT-4o, and GPT-4o-mini, and 100% on medium 7/7 for all four listed models except CodeLlama’s easy result of 4/5 (80%). Its best easy verifiable rate was 68% and pass rate 50% with GPT-4o; best medium verifiable rate was 42.3% and pass rate 28.6% with GPT-4o (Table III, pp. 6–7). These denominators are task counts, while verifiable/pass percentages summarize property/code thresholds.
Efficiency Table I records attempts among cases passing syntax. For Agents4PLC, DeepSeek V2.5, GPT-4o, and GPT-4o-mini each passed syntax on the first attempt for 16/16 easy and 7/7 medium; CodeLlama passed 4/5 easy on first attempt and 1/1 medium (Table I, p. 8). The ablation (Table II, p. 8) reports, for easy tasks, full one-shot+RAG+syntax-hint GPT-4o configuration at 16/16 syntax, 8/16 pass (50.0%), and 11/16 verifiable (68.8%); removing RAG gave 11/16 pass (68.8%) and 12/16 verifiable (75.0%), showing that components do not help uniformly. For medium tasks, the full configuration achieved 7/7 syntax, 2/7 pass (28.6%), and 3/7 verifiable (42.9%). The study uses PLC model checking and practical UWinTech case studies, not Rust or Verus proofs.
proved, trusted, and product threat
Measured: benchmark syntax, verifiability, pass rates, attempt counts, ablations, and case studies. Trusted: human-written formal specifications and reference code, LLM-generated properties when inputs lack them, ST-to-SMV/CBMC translation, model-checker assumptions, and the adequacy of natural-language requirements. The paper itself notes translation inconsistency and state explosion. Inference: the main threat to VL is accepting a generated contract or translation as if it were the user’s intent; an agent may “verify” the wrong property. VL should retain a human/specification authority boundary, direct Verus checking, exact source-to-proof provenance, and a loop bound/escalation policy. Existing multi-agent PLC workflows already cover role separation, RAG, compiler feedback, model checking, and repair; VL should not duplicate those generic orchestration claims without Rust/Verus-specific evidence.
techniques for the catalog
- role-separated closed loop: retrieval and planning guide coding, compiler checks syntax, validation checks properties, and debugging repairs failures
- RAG plus domain prompts: retrieve IEC/ST examples and encode safety/compiler constraints in generation and repair prompts
- property generation: derive verifier-format properties from requirements when absent, subject to human/specification trust
- translation-based model checking: map ST to SMV/CBMC and run model checking or BMC while tracking translation and state-explosion risks
- thresholded repair: iterate diagnostics-driven fixes until success or loop threshold, then select another plan or escalate Checked 2026-10-14 against the paper by a Codex agent: audit record liu2024agents4plc; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments
Last edited: