Korrekte Codegeneratoren für speicherprogrammierbare Steuerungen

Speicherprogrammierbare Steuerungen werden eingesetzt, um technische Prozesse zu steuern. Da diese oft in sicherheitskritischen Bereichen sind die Anforderungen an Zuverlässigkeit und Korrektheit der Software für speicherprogrammierbare Steuerungen sehr hoch. Die typische Vorgehensweise zum Entwurf solcher Software erstellt zunächst eine Spezifikation (basierend auf endlichen Automaten oder Petri-Netzen), die dann auf Sicherheitsbedingungen geprüft wird und anschliessend durch Codegeneratoren in ablauffähigen Code transformiert wird. Ohne die Korrektheit dieser Codegeneratoren kann nicht auf die Korrektheit des Codes (insbesondere auch bzgl. der Sicherheitsbedingungen) geschlossen werden. Das Ziel des Projekts ist es, diese Lücke zu schliessen. Dazu sollen Methoden, die im Rahmen des DFG-Projektes Verifix zur Konstruktion korrekter Übersetzer entwickelt wurden, auf die spezifischen Anforderungen der Programmierung speicherprogrammierbarer Steuerungen angepasst werden.