EVENT

ERATO Project Colloquium by Ignacio D. Lopez-Miguel

On Tuesday 1 October, Ignacio D. Lopez-Miguel (Vienna University of Technology) will give a talk, "Formal verification and specification of PLC programs. Lessons learned from CERN.", for our project colloquium at 16:30.Further details can be found below.

Title:

Formal verification and specification of PLC programs. Lessons learned from CERN.

Speaker:

Ignacio D. Lopez-Miguel (Vienna University of Technology) Title: Formal verification and specification of PLC programs. Lessons learned from CERN.

Abstract:

CERN is a physics lab with the largest particle accelerator in the world. A failure in one of its systems can be catastrophic, stopping data generation for up to a year.
Programmable logic controllers are industrial computers designed to work under extreme situations and are thus suitable for CERN purposes. However, not only does their hardware need to be robust, but so does their code. In order to ensure this, formal verification of some of their systems is performed using an in-house developed tool named PLCverif. However, it is only possible to verify a program if there is a formal specification, which is usually the biggest problem.
In this talk, I will share my experience formally verifying PLC programs for CERN and GSI, as well as collaborating with NASA AMES to integrate their tool to write formal requirements, FRET, into PLCverif.

Time/Date:

16:30- / Tuesday 1 October,2024

Place:

NII Room 1310A and Online

Link:

For the latest information about ERATO colloquium/seminar, please see the webpage.
https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpXDeA/edit

Contact:

Kittiphon Phalakarn (ERATO MMSD Colloquium Organizer)
Email: kphalakarn[at] nii.ac.jp