format_version: "0.1"
id: g_tank_valves
name: "Tank valve controller — valves handler (graphical LD)"
domain: water_treatment
language: LD-graphical
source:
  origin: plc-ld-dataset
  reference: "PLC-LD-dataset, github.com/UniboSecurityResearch/PLC-LD-dataset (Iacobelli et al., ICPS 2024, doi:10.1109/ICPS59941.2024.10639995); legitimate/malicious LLB pair, PLCopen XML"
  license: "GPL-3.0"
properties_file: props.yaml
safety_intent: "Every PLC scan cycle must complete; no while-loop may run without its counter advancing, which would hang the scan."
validation_status: candidate
variants:
  - file: legitimate_lvalves_handler.xml
    expected_verdict: true
    ground_truth:
      method: cross-tool-consensus
      confirmed_by: [esbmc-plc+]
  - file: malicious_mvalves_handler.xml
    expected_verdict: false
    violated_properties: [P1]
    ground_truth:
      method: fault-injection
      base_variant: legitimate_lvalves_handler.xml
      seeded_defect: "Injected non-terminating while-loop (loop counter never incremented), gated on a trigger sensor value."
      witness: "A trigger input (e.g. IN1=12) enters the loop that never exits; the scan-watchdog flags the hang."
features: [contacts, coils, function_block, comparison]
difficulty: medium
tags: [security, llb, non-termination]