Title: Formal Verification of PLC Software Evolution Across Migration and Upgrade

Speaker: Soumyadip Bandyopadhyay    (bio) (bio)

Soumyadip Bandyopadhyay is an industrial researcher and engineer specializing in verification and evolution of safety-critical automation software. He currently works at ABB, contributing to the development and validation of industrial control systems based on Programmable Logic Controllers (PLC) and Distributed Control Systems (DCS). His work focuses on ensuring correctness, reliability, and safe modernization of legacy control software through formal verification, behavioral equivalence checking, and automated software migration techniques. With prior experience as an Assistant Professor at BITS Pilani and a postdoctoral researcher at the Hasso Plattner Institute, Germany, he bridges academic research and industrial practice. His interests include formal methods for industrial automation, trustworthy AI for engineering workflows, and verification of software upgrades in large-scale industrial systems.

When: Tuesday, 12 May 2026 at 1900 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
Industrial plants rely on Programmable Logic Controllers (PLC) and Distributed Control Systems (DCS) for automation. As industrial requirements evolve, control software undergoes migration from legacy languages such as Taylor™ Control Language (TCL) to IEC 61131-3 compliant Sequential Function Charts (SFC), as well as upgradation of existing SFC programs through the addition of new features. Both processes risk introducing unintended behavioural deviations that may compromise safety. This work addresses automatic behavioural verification during PLC software evolution. We present a Petri net based framework that models TCL and SFC programs as formal behavioural representations. The approach verifies behavioural equivalence for migration and checks containment between older and upgraded SFC versions using a symbolic path-based equivalence checking algorithm, ensuring the preservation of existing functionality while accommodating new features.