Analyse bedingter Software-Spezifikationen für Speicherprogrammierbare Steuerungen

• Antragsteller: Professor Dr.-Ing. Stefan Kowalewski
• Fachliche Zuordnung: Automatisierungstechnik, Mechatronik, Regelungssysteme, Intelligente Technische Systeme, Robotik
• Förderung: Förderung von 2017 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 335714914

Dieses Projekt befasst sich mit bedingten Software-Spezifikationen für Speicherprogrammierbare Steuerungen (SPS) und mit der effizienten Fehlersuche darin. Bedingte Spezifikationen entstehen, wenn die Anforderungen an die Gesamtsteuerung auf Verhaltensanforderungen für Komponenten heruntergebrochen werden, wobei zwischen "Garantien" zum Verhalten von Komponenten bzw. Funktionsblöcken und "Annahmen" zum Verhalten ihrer Umgebung unterschieden wird. Im Gegensatz zur Verifikation von Implementierungen oder implementierungsnahen Modellen, deren Verhalten gegen eine getrennt entstandene Anforderung geprüft wird, ist hier zu analysieren, ob die Dekomposition einer formalen Anforderung an das System in eine Menge von Komponenten-Anforderungen die ursprüngliche, übergeordnete Anforderung impliziert. In dem beantragten Projekt soll ein algorithmisches, skalierbares Verfahren entstehen, mit dem durch falsche Dekomposition entstandene Inkonsistenzen in Software-Spezifikationen für SPSen frühzeitig gefunden werden können. Die (vollständige) Verifikation mit zeitbehafteten For-malismen ist, bedingt durch die zusätzlichen Zustände der Uhrenvariablen, notorisch schwierig. Da es darauf ankommt, Spezifikationsfehler möglichst rasch zu finden ohne den gesamten Zustandsraum zu durchsuchen, setzen wir unvollständige Methoden ein. Die hier betrachteten bedingten Spezifikationen bestehen aus einer Bedingung, die ein erwartetes Verhalten der Umgebung einer Komponente festlegt ("Annahme") und einer Bedingung zum Verhalten der Komponente selbst ("Garantie"), die nur dann erfüllt sein muss, wenn das Umgebungsverhalten der zugehörigen Annahme entspricht. Teilspezifikationen werden als "Observer-Automaten" modelliert und die Falsifizierung mit Hilfe von Modellprüfung durchgeführt. Da sich die bei der Verifikation von implementierungsnahen Modellen bewährten Abstraktionsverfahren auf Anforderungen im Allgemeinen nicht anwenden lassen, sind neue Ansätze zur Steigerung von Effizienz und Skalierbarkeit notwendig. Hierzu setzen wir gerichtetes (engl. directed/guided) Model-Checking ein. Wir werden erstmals den Zusammenhang zwischen einer übergeordneten bedingten Anforderung und ihrer Dekomposition zur Definition von Maßen nutzen, auf deren Grundlage Heuristiken für ein schnelleres Erreichen der Zielzustände bzw. Spezifikationsfehler abgeleitet werden können. Besonders wichtig ist, dass dies gelingt, ohne ein explizites Produkt von Observer-Automaten zu erstellen.

• DFG-Verfahren: Sachbeihilfen