Formal Verification in Automated Manufacturing

Beschreibung

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.