51²è¹Ý

Zoom Link: https://zoom.us/j/92318501118?pwd=Msjgq8aTadSNH8PIisiaWFhF4vtBWa.1

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 talk, 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. Experimental evaluation on 80 real-world benchmarks from the OSCAT library highlights the effectiveness of the framework. We have compared our approach with verifAPS, a popular tool used for software upgradation, and observed nearly 4x performance improvement.

About the Speaker: Soumyadip Bandyopadhyay is a Scientist at ABB Corporate Research, working on formal verification of PLC software, validation of Generative AI outputs, and LLM-driven forward engineering. He holds a Ph.D. from IIT Kharagpur in Formal Methods and Software Engineering, and was a Postdoctoral Researcher at the Hasso Plattner Institute, Germany. He previously served as an Assistant Professor at BITS Pilani, Goa, and later worked as a Senior Formal Verification Engineer at NVIDIA, focusing on datapath verification.

We look forward to your active participation.