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.