Formal Verification in Automated Manufacturing

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.