Verifying Correctness of PLC Software during System Evolution using Model Containment Approach
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911141076140032 |
|---|---|
| author | Bandyopadhyay, Soumyadip Sarkar, Santonu |
| author_facet | Bandyopadhyay, Soumyadip Sarkar, Santonu |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_05596 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verifying Correctness of PLC Software during System Evolution using Model Containment Approach Bandyopadhyay, Soumyadip Sarkar, Santonu Software Engineering Symbolic Computation 68 D.3.1; D.2.4 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. |
| title | Verifying Correctness of PLC Software during System Evolution using Model Containment Approach |
| topic | Software Engineering Symbolic Computation 68 D.3.1; D.2.4 |
| url | https://arxiv.org/abs/2509.05596 |