Dear all,
The next talk in the IARCS Verification Seminar Series will be given by
Soumyadip Bandyopadhyay, an industrial researcher and engineer at ABB,
specializing in verification and evolution of safety-critical automation
software.. The talk is scheduled on Tuesday, May 12, at 1900 hrs IST (add
to Google calendar
<https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NDR2dTZtcnY1dXBhOWViNWdyc3JuMDE1bm8gdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com>
).
The details of the talk can be found on our webpage (
https://fmindia.cmi.ac.in/vss/), and also appended to the body of this
email.
The Verification Seminar Series, an initiative by the Indian Association
for Research in Computing Science (IARCS), is a monthly, online
talk-series, broadly in the area of Formal Methods and Programming
Languages, with applications in Verification and Synthesis. The aim of this
talk-series is to provide a platform for Formal Methods researchers to
interact regularly. In addition, we hope that it will make it easier for
researchers to explore newer problems/areas and collaborate on them, and
for younger researchers to start working in these areas.
All are welcome to join.
Best regards,
Organizers, IARCS Verification Seminar Series
=============================================================
Title: Formal Verification of PLC Software Evolution Across Migration and
Upgrade
Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting 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.
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.