2025/09/06 by Soumyadip Bandyopadhyay, Bandyopadhyay, Soumyadip, Santonu Sarkar +1
Computer Science · #68 #D.2.4 #D.3.1 #FOS: Computer and information sciences #Software Engineering (cs.SE) #Software Engineering Research #Software Reliability and Analysis Research #Software System Performance and Reliability #Symbolic Computation (cs.SC)
paper · pdf · doi:10.48550/arxiv.2509.05596
openalex publication_date 2025/09/06 · openalex created_date 2025/10/11 · openalex updated_date 2026/07/28
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.