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

点击翻译按钮获取中文摘要

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.