A case study in compositional model-checking of hierarchical PLC programs

Abstract

In the world today, software is everywhere. Thus, maintaining the assurance that the software a person is using is safe and of high quality is imperative. Software for controlling a plant or production facility is often placed in a programmable logic controller (PLC), a robust and reliable embedded controller. Currently, manual testing, which often turns out to be sensitive to errors, is generally used to ensure the quality and safety of PLC programs.
Use of model checking for PLC programs could alleviate this problem of error sensitivity by exploring all possible states of the software. An often-discussed challenge is that of the state space explosion when model checking PLC programs, for example. This research focuses on the idea that the hierarchical structure of Siemens PLC programs can be leveraged to apply compositional model checking. Current studies demonstrate the model checking of
small lab test scale case studies, and only a handful of studies reveal the model checking of an industrial-sized PLC program in case studies. None of the studies apply compositional model checking to PLC programs. This research presents a novel approach to model checking PLC programs through the addition of compositional reasoning to the model checking of industrial-sized Siemens PLC programs. The presented approach demonstrates successful compositional verification of an industrial-sized PLC program.

Date of Award	13 Oct 2021
Original language	English
Supervisor	Freek Verbeek (Examiner) & Stefano Schivo (Supervisor)