Statische Analyse von GRAFCET-Spezifikationen zur Erkennung von Entwurfsfehlern
Publication date
2025-01-02
Document type
Dissertation
Author
Advisor
Referee
Kowalewski, Stefan
Granting institution
Helmut-Schmidt-Universität / Universität der Bundeswehr Hamburg
Exam date
2025-12-18
Organisational unit
Project
AGRAFE - Analyse von GRAFCET-Spezifikationen zur Erkennung von Entwurfsfehlern
Publisher
Universitätsbibliothek der HSU/UniBw H
Part of the university bibliography
✅
File(s)
Language
German
Keyword
GRAFCET
formale Methoden
abstrakte Interpretation
Steuerungsentwurf
Abstract
Mit dem intensiven Einsatz von automatisierten Produktionsanlagen muss sichergestellt werden, dass diese ihre Dienste korrekt bereitstellen und dass das von ihnen ausgehende Risiko keine Gefahr für die Sicherheit von Personen und der Umwelt darstellt. Daher ist es das Ziel dieser Arbeit, einen Verifikationsansatz zu erforschen, der während der Entwicklung solcher Produktionssysteme eingesetzt werden kann, um das Steuerungsverhalten dieser Systeme sicherer zu machen. GRAFCET wurde als geeignetes Beschreibungsmittel für ein solches Steuerungsverhalten identifiziert, und es wurde die statische Analyse als geeigneter Verifikationsansatz identifiziert.
Das formulierte Forschungsziel wurde in vier Teilforschungsfragen gegliedert, wozu jeweils ein Forschungsartefakt erstellt wurde. Die Forschungsfragen und -artefakte befassen sich mit der Interpretation der GRAFCET-Norm, der Frage nach geeigneten Eigenschaften, die die Steuerungsspezifikationen aufweisen müssen, sowie der Sicherstellung syntaktischer und semantischer Korrektheit der Steuerungsspezifikationen. Während der Evaluation wurde anhand von zwei Anwendungsbeispielen geprüft, ob diese Forschungsartefakte die Forschungsfragen beantworten können und insbesondere, ob der entwickelte Verifikationsansatz dazu geeignet ist, Eigenschaften in den Spezifikationen nachzuweisen, und ob das Skalierungsverhalten der Algorithmen eine Limitation darstellt. Ergebnis ist, dass die erforschte statische Analyse eine Überapproximation des tatsächlichen Steuerungsverhaltens erzeugt, wodurch das Skalierungsverhalten so gut ist, dass auch große Spezifikationen verifiziert werden können. Weiter ist es mit dem vorgestellten Ansatz möglich, eine Klasse von Eigenschaften der Spezifikationen nachzuweisen und so die Sicherheit des Anlagenverhaltens zu verbessern. Allerdings führt die Überapproximation dazu, dass die Analyse abhängig von den Elementen in der vorliegenden Spezifikation und abhängig von der zu verifizierenden Eigenschaft auch falsche Antworten hervorbringt. Dieses Verhalten muss bei der Interpretation der Ergebnisse berücksichtigt werden.
Für künftige Forschungen ist eine Kombination von statischer Analyse mit anderen Verifikationstechniken wie dem Model Checking vielversprechend, um die Vorteile beider Ansätze nutzen zu können.
Das formulierte Forschungsziel wurde in vier Teilforschungsfragen gegliedert, wozu jeweils ein Forschungsartefakt erstellt wurde. Die Forschungsfragen und -artefakte befassen sich mit der Interpretation der GRAFCET-Norm, der Frage nach geeigneten Eigenschaften, die die Steuerungsspezifikationen aufweisen müssen, sowie der Sicherstellung syntaktischer und semantischer Korrektheit der Steuerungsspezifikationen. Während der Evaluation wurde anhand von zwei Anwendungsbeispielen geprüft, ob diese Forschungsartefakte die Forschungsfragen beantworten können und insbesondere, ob der entwickelte Verifikationsansatz dazu geeignet ist, Eigenschaften in den Spezifikationen nachzuweisen, und ob das Skalierungsverhalten der Algorithmen eine Limitation darstellt. Ergebnis ist, dass die erforschte statische Analyse eine Überapproximation des tatsächlichen Steuerungsverhaltens erzeugt, wodurch das Skalierungsverhalten so gut ist, dass auch große Spezifikationen verifiziert werden können. Weiter ist es mit dem vorgestellten Ansatz möglich, eine Klasse von Eigenschaften der Spezifikationen nachzuweisen und so die Sicherheit des Anlagenverhaltens zu verbessern. Allerdings führt die Überapproximation dazu, dass die Analyse abhängig von den Elementen in der vorliegenden Spezifikation und abhängig von der zu verifizierenden Eigenschaft auch falsche Antworten hervorbringt. Dieses Verhalten muss bei der Interpretation der Ergebnisse berücksichtigt werden.
Für künftige Forschungen ist eine Kombination von statischer Analyse mit anderen Verifikationstechniken wie dem Model Checking vielversprechend, um die Vorteile beider Ansätze nutzen zu können.
Version
Published version
Access right on openHSU
Open access