Formal Verification in Automated Manufacturing

In recent decades, discrete-event modelling has been widely utilised to address control engineering
problems. Comparing with conventional dynamic system modelling where physical behaviour is
explicitly to describe, discrete-event modelling focuses on a more abstract level where logical
behaviour is of interest. In this dissertation, we focus on the formal verification of the logical closedloop
behaviour of control systems. To satisfy safety and/or liveness requirements according to given
technical specifications, we exploit the formal semantics of control programmes to represent the
entire closed-loop behaviour in a discrete-event model, from which the properties of interest can be
formally verified through an efficient method. In den letzten Jahrzehnten wurde die ereignisdiskrete Modellierung immer öfter angewandt, um
regelungstechnische Probleme zu behandeln. Im Vergleich zur konventionellen
Modellierung von dynamischen Systemen, wobei physikalisches Verhalten explizit zu beschreiben
ist, konzentriert sich die ereignisdiskrete Modellierung auf eine abstraktere Ebene, auf der logisches
Verhalten von Interesse ist. In dieser Dissertation konzentrieren wir uns auf die formale Verifikation
des logischen Verhaltens von Regelkreisen. Um Sicherheits- und/oder Lebendigkeitsanforderungen
anhand gegebener technischer Spezifikationen zu gewährleisten, verwenden wir die formale
Semantik von Steuerprogrammen, um den gesamten geschlossenen Regelkreis von einem
ereignisdiskreten System darzustellen, so dass die interessierenden Eigenschaften formal durch eine
effiziente Methode verifiziert werden können.