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

• Erstellungsjahr: 2016

Zusammenfassung der Projektergebnisse

In dem Projekt wurde ein Ansatz zum direkten Model-Checking von Steuerungssoftware (d.h. ohne Notwendigkeit der Modellierung des Programms) auf Programme für Speicherprogrammierbare Steuerungen (SPSen) übertragen und algorithmisch wesentlich erweitert, um die Effizienz und Anwendbarkeit auf industrielle SPS-Programme zu verbessern. Folgende neue algorithmische Ansätze wurden erarbeitet. Es wurden mehrere Abstraktionsverfahren entwickelt, mit denen der zu durchsuchende Zustandsraum verkleinert werden kann, ohne relevante Eigenschaften zu verlieren. Dabei wurde zum ersten Mal das Prinzip der Gegenbeispiel-geleiteten Abstraktionsverfeinerung auf SPS-Code angewendet. Zur Reduktion des Suchraums beim Model-Checking wurden Techniken aus der Statischen Analyse, u.a. Slicing, erfolgreich übertragen. Die Statische Analyse von SPS-Code konnte durch die automatische Ableitung von Transferfunktionen für Schleifen in Programmen wesentlich vereinfacht werden. Weitere Ergebnisse ermöglichen, die automatische statische Wertebereichsanalyse für Variablen in SPS-Programmen und Modelle der Steuerstrecke zu erstellen und in das Model-Checking zu integrieren. Alle entstandenen Techniken wurde in dem Werkzeug A RCADE prototypisch implementiert und an industriellen oder industrietypischen Steuerungsprogrammen evaluiert. Im Ergebnis liegt eine werkzeuggestützte Umgebung für die Korrektheitsanalyse von SPS-Code vor, die wesentliche methodische Fortschritte im Vergleich zum Stand der Technik vor Beginn des Projekts realisiert.

Projektbezogene Publikationen (Auswahl)

• Counterexample-guided abstraction refinement for PLCs. In: 5th International Workshop on Systems Software Verification (SSV 2010), Vancouver, Canada. Berkeley, CA, USA : USENIX Association, 2010, S. 2–12
  Biallas, S. ; Brauer, J. ; Kowalewski, S.
  
• Arcade.PLC: A Verification Platform for Programmable Logic Controllers. In: Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, ACM, 2012 (ASE 2012). – ISBN 978–1–4503–1204–2, S. 338–341
  Biallas, S. ; Brauer, J. ; Kowalewski, S.
  
• Loop Leaping with Closures. In: M INÉ, Antoine (Hrsg.) ; Schmidt, David (Hrsg.): 19th Static Analysis Symposium, Springer Berlin Heidelberg, 2012 (Lecture Notes in Computer Science). – ISBN 978–3–642–33124–4, S. 214–230
  Biallas, S. ; Brauer, J. ; King, A. ; Kowalewski, S.
  
• Boolean and Modular Abstractions for Programmable Logic Controllers. In: Dependable Control of Discrete Systems (DCDS’13), IEEE, 2013. – ISBN 978–3–902823–49–6, S. 97–102. – Best paper award
  Biallas, S. ; Bohlender, D. ; Kowalewski, S.
  
• Predicate Abstraction for Programmable Logic Controllers. In: Pecheur, Charles (Hrsg.) ; Dierkes, Michael (Hrsg.): 18th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2013) Bd. 8187, Springer Berlin Heidelberg, 2013 (Lecture Notes in Computer Science 8187). – ISBN 978–3–642–41009–3, S. 123–138
  Biallas, S. ; Giacobbe, M. ; Kowalewski, S.
  
• Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code. In: Proceedings of the 12th International Workshop on Discrete Event Systems. Cachan, France : IFAC, 2014, S. 400–405
  Biallas, Sebastian ; Kowalewski, Stefan ; Stattelmann, Stefan ; Schlich, Bastian