Verifikation von Programmen für speicherprogrammierbare Steuerungen mit Hilfe statischer Analyse und direktem Model-Checking

• Antragsteller: Professor Dr.-Ing. Stefan Kowalewski, seit 3/2010
• Fachliche Zuordnung: Automatisierungstechnik, Mechatronik, Regelungssysteme, Intelligente Technische Systeme, Robotik
• Förderung: Förderung von 2009 bis 2013
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 160687124

Das Ziel des Projektes besteht in der Erarbeitung einer neuen Methodik zur formalen Verifikation von Programmen für speicherprogrammierbare Steuerungen (SPSen). Der zu entwickelnde Ansatz soll sich an dem von uns entwickelten Ansatz zur Verifikation von Assembler-Programmen für Mikrocontroller orientieren. Die drei zentralen Bestandteile dieses Ansatzes sind die direkte Anwendung von Model-Checking, die Kombination unterschiedlicher formaler Methoden und die Verwendung hardwareabhängiger Informationen in diesen Methoden. Im Unterschied zu den bekannten Ansätzen soll die Methodik keinen Übersetzungsschritt in die Eingabeformalismen existierender Werkzeuge benötigen, sondern das Model-Checking direkt auf dem SPS-Programm ausführen. Die Kombination von statischer Analyse, abstrakter Interpretation und Model-Checking soll die Behandlung größerer Programme erlauben, als dies zurzeit möglich ist, um einer industriellen Anwendbarkeit näher zu kommen. Innerhalb dieser Methoden sollen Informationen über SPSen und die jeweiligen Programmiersprachen genutzt werden, um die Komplexität der zu lösenden Probleme zu begrenzen und Aussagen über spezifische Details der SPSen und der Programme zu erlauben.

• DFG-Verfahren: Sachbeihilfen
• Ehemaliger Antragsteller: Dr. Bastian Schlich, von 8/2009 bis 2/2010