Verifying Correctness of PLC Software during System Evolution using Model Containment Approach

• URL: http://arxiv.org/abs/2509.05596v1
• Date: Sat, 06 Sep 2025 04:45:17 GMT
• Title: Verifying Correctness of PLC Software during System Evolution using Model Containment Approach
• Abstract summary: We propose a verification-based approach to ensure the correctness of the upgraded version of a PLC software.<n>We have developed a home-grown Petri net-based containment checker.<n>We have compared our approach with verifAPS, a popular tool used for software upgradation, and observed nearly 4x performance improvement.
• Score: 22.261628532402067
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Upgradation of Programmable Logic Controller (PLC) software is quite common to accommodate evolving industrial requirements. Verifying the correctness of such upgrades remains a significant challenge. In this paper, we propose a verification-based approach to ensure the correctness of the existing functionality in the upgraded version of a PLC software. The method converts the older and the newer versions of the sequential function chart (SFC) into two Petri net models. We then verify whether one model is contained within another, based on a novel containment checking algorithm grounded in symbolic path equivalence. For this purpose, we have developed a home-grown Petri net-based containment checker. Experimental evaluation on 80 real-world benchmarks from the OSCAT library highlights the scalability and effectiveness of the framework. We have compared our approach with verifAPS, a popular tool used for software upgradation, and observed nearly 4x performance improvement.

Related papers

• REVES: REvision and VErification--Augmented Training for Test-Time Scaling [53.197756110943395]
  We propose a two-stage iterative framework that alternates between online data/prompt augmentation and policy optimization.<n>We observe gains of +6.5 points over the RL baseline and +4.0 points over standard multi-turn training.
  arXiv  Detail & Related papers  (2026-06-17T10:37:23Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoder is an agentic code verification framework.<n>It enables prove-as-you-generate development where code, invariants, and proofs co-evolve.
  arXiv  Detail & Related papers  (2026-03-31T00:06:44Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  silicon-grade correctness remains bottlenecked by: (i) limited test coverage and reliability of simulation-centric evaluation, (ii) regressions and repair hallucinations, and (iii) semantic drift as intent is reinterpreted across agent handoffs.<n>We propose Veri-Sure, a multi-agent framework that establishes a design contract to align agents' intent and uses a patching mechanism guided by static dependency slicing to perform precise, localized repairs.
  arXiv  Detail & Related papers  (2026-01-27T16:10:23Z)
• Plug-and-Play Benchmarking of Reinforcement Learning Algorithms for Large-Scale Flow Control [61.155940786140455]
  Reinforcement learning (RL) has shown promising results in active flow control (AFC)<n>Current AFC benchmarks rely on external computational fluid dynamics (CFD) solvers, are not fully differentiable, and provide limited 3D and multi-agent support.<n>We introduce FluidGym, the first standalone, fully differentiable benchmark suite for RL in AFC.
  arXiv  Detail & Related papers  (2026-01-21T14:13:44Z)
• Autonomous Issue Resolver: Towards Zero-Touch Code Maintenance [0.0]
  We propose a paradigm shift from the standard Code Property Graphs to the concept of Data Transformation Graph (DTG)<n>We introduce a multi-agent framework that reconciles data integrity navigation with control flow logic.<n>Our approach has demonstrated good results on several SWE benchmarks, reaching a resolution rate of 87.1%.
  arXiv  Detail & Related papers  (2025-12-09T11:11:37Z)
• Continual Action Quality Assessment via Adaptive Manifold-Aligned Graph Regularization [53.82400605816587]
  Action Quality Assessment (AQA) quantifies human actions in videos, supporting applications in sports scoring, rehabilitation, and skill evaluation.<n>A major challenge lies in the non-stationary nature of quality distributions in real-world scenarios.<n>We introduce Continual AQA (CAQA), which equips with Continual Learning capabilities to handle evolving distributions.
  arXiv  Detail & Related papers  (2025-10-08T10:09:47Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  Test-time algorithms that combine the generative power of language models with process verifiers offer a promising lever for eliciting new reasoning capabilities.<n>We introduce a new process-guided test-time sampling algorithm, VGB, which uses theoretically grounded backtracking to achieve provably better robustness to verifier errors.
  arXiv  Detail & Related papers  (2025-10-03T16:21:14Z)
• Machine Learning Pipeline for Software Engineering: A Systematic Literature Review [0.0]
  This systematic literature review examines state-of-the-art Machine Learning pipelines designed for software engineering (SE)<n>Our findings show that robust preprocessing, such as SMOTE for data balancing, improves model reliability.<n> Ensemble methods like Random Forest and Gradient Boosting dominate performance across tasks.<n>New metrics like Best Arithmetic Mean (BAM) are emerging in niche applications.
  arXiv  Detail & Related papers  (2025-07-31T15:37:30Z)
• VeriReason: Reinforcement Learning with Testbench Feedback for Reasoning-Enhanced Verilog Generation [9.07044866283158]
  We introduce VeriReason, a framework integrating supervised fine-tuning with Guided Reward Proximal Optimization (GRPO) reinforcement learning for RTL generation.<n>On the VerilogEval Benchmark, VeriReason delivers 83.1% functional correctness, substantially outperforming both comparable-sized models and much larger commercial systems like GPT-4 Turbo.<n>VeriReason represents the first system to successfully integrate explicit reasoning capabilities with reinforcement learning for Verilog generation, establishing a new state-of-the-art for automated RTL synthesis.
  arXiv  Detail & Related papers  (2025-05-17T05:25:01Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  We propose a unified Test-Time Compute scaling framework that leverages increased inference-time instead of larger models.<n>Our framework incorporates two complementary strategies: internal TTC and external TTC.<n>We demonstrate our textbf32B model achieves a 46% issue resolution rate, surpassing significantly larger models such as DeepSeek R1 671B and OpenAI o1.
  arXiv  Detail & Related papers  (2025-03-31T07:31:32Z)
• Agents4PLC: Automating Closed-loop PLC Code Generation and Verification in Industrial Control Systems using LLM-based Agents [27.097029139195943]
  Agents4PLC is a novel framework that automates PLC code generation and code-level verification.<n>We first establish a benchmark for verifiable PLC code generation area.<n>We then transition from natural language requirements to human-written-verified formal specifications and reference PLC code.
  arXiv  Detail & Related papers  (2024-10-18T06:51:13Z)
• CodeDPO: Aligning Code Models with Self Generated and Verified Source Code [52.70310361822519]
  We propose CodeDPO, a framework that integrates preference learning into code generation to improve two key code preference factors: code correctness and efficiency.<n>CodeDPO employs a novel dataset construction method, utilizing a self-generation-and-validation mechanism that simultaneously generates and evaluates code and test cases.
  arXiv  Detail & Related papers  (2024-10-08T01:36:15Z)
• Uncovering the Hidden Cost of Model Compression [43.62624133952414]
  Visual Prompting has emerged as a pivotal method for transfer learning in computer vision. Model compression detrimentally impacts the performance of visual prompting-based transfer. However, negative effects on calibration are not present when models are compressed via quantization.
  arXiv  Detail & Related papers  (2023-08-29T01:47:49Z)
• Consensus-Adaptive RANSAC [104.87576373187426]
  We propose a new RANSAC framework that learns to explore the parameter space by considering the residuals seen so far via a novel attention layer. The attention mechanism operates on a batch of point-to-model residuals, and updates a per-point estimation state to take into account the consensus found through a lightweight one-step transformer.
  arXiv  Detail & Related papers  (2023-07-26T08:25:46Z)
• Model-based adaptation for sample efficient transfer in reinforcement learning control of parameter-varying systems [1.8799681615947088]
  We leverage ideas from model-based control to address the sample efficiency problem of reinforcement learning algorithms. We demonstrate that our approach is more sample-efficient than fine-tuning with reinforcement learning alone.
  arXiv  Detail & Related papers  (2023-05-20T10:11:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.