The following technical report is available from http://aib.informatik.rwth-aachen.de:

Runtime Supervision of PLC Programs Using Discrete-Event Systems Florian Göbe AIB 2019-05

The supervisory control theory (SCT) introduced by Ramadge and Wonham is one of the most noted formalisms for the synthesis of solutions in discrete event control. In this dissertation, an approach is elaborated which applies the SCT framework for the supervision of arbitrary existing PLC controller programs. The latter are assumed to be provided manually by the user and hence are not formally guaranteed to respect certain constraints, such as demands on safety, in all possible situations. With the presented approach, these conditions can be formulated in form of discrete-event systems. Using adaptations of the Ramadge and Wonham framework, a supervision layer is generated from these models. It prevents the controller from executing critical actions during runtime, which could eventually lead to the violation of the specified requirements.

In order to address a wide range of realistic use cases, several adaptations and extensions have been introduced to the original framework, such as conditional transitions, templates and event enforcement for the preemption of undesired incidents. A concept for an end-to-end solution from the creation of the requirement models to a ready-to-use safety layer is presented and has been implemented in a tool.

The suitability of the concept has been evaluated in several case studies, some on industrial hardware. Furthermore, the usability of the approach as a whole, the introduced modifications and the tool implementation have been evaluated in a user study.