In diesem Projekt soll eine formale Beschreibung von Steuerungsabl\u00e4ufen mithilfe der Spezifikationssprache GRAFCET erreicht werden. Darauf aufbauend sollen die M\u00f6glichkeiten f\u00fcr formale Verifikationen dieser Spezifikationen untersucht werden, um die Entwurfsphase im Engineeringprozess zu unterst\u00fctzen. Dieses Projekt baut damit auf den Ergebnissen des, ebenfalls von der DFG gef\u00f6rderten, Projekts \u201eGRAFCETbringtS\u201c auf.<\/p>\n
GRAFCET (IEC 60848) ist ein graphisches Beschreibungsmittel zur Spezifikation von Steuerungsabl\u00e4ufen. GRAFCET adaptiert daf\u00fcr Konzepte aus dem Bereich der Petri-Netze. Neben den Basiselementen (Schritte und Transitionen) und sequenziellen, alternativen oder parallelen Abl\u00e4ufen k\u00f6nnen mit GRAFCET auch hierarchische Strukturen abgebildet werden. So ist es m\u00f6glich, Teile der Steuerung in eine bestimmte Situation zu zwingen, was GRAFCET von anderen Beschreibungssprachen abhebt.<\/p>\n
Im Laufe des Entwurfsprozesses einer Automatisierungsl\u00f6sung wird u.a. das Sollverhalten des Systems in Bezug auf logische Zusammenh\u00e4nge und Abl\u00e4ufe festgelegt. Mit Blick auf das Gesamtsystem stellt die Spezifikation somit eine wichtige Vorstufe zur Implementierung und Realisierung von Steuerungen dar. Da der Steuerungsentwurf oftmals intuitiv, ohne formelle Beschreibung oder Dokumentation und ohne vollst\u00e4ndige Validierung der Entwurfsergebnisse erfolgt, ist die Verwendung von geeigneten, regelbasierten Methoden unabdingbar.<\/p>\n
Im Rahmen des systematischen Steuerungsentwurfes im Bereich der Spezifikation und Implementierung werden innerhalb dieses Forschungsschwerpunktes formale Beschreibungsmittel untersucht. Dabei sind die Fragestellungen zentral, wie diese formalen Beschreibungsmittel eindeutig und regelbasiert in Steuerungscode umgesetzt werden k\u00f6nnen. Und darauf aufbauend, wie Entwurfsfehler, unabh\u00e4ngig von der Steuerstrecke mithilfe formaler Methoden erkannt werden k\u00f6nnen. Dabei sollen sowohl statische Analysen, als auch Model Checking zum Einsatz kommen.<\/p>\n