Speicherprogrammierbare Steuerungen (PLCs) werden häufig im industriellen Umfeld in sicherheitskritischen Systemen eingesetzt. Für [mc]square, einem Model-Checker zur Verifikation von Mikrocontroller-Software, unterstützen wir Programme für PLCs, die in der Sprache Anweisungsliste (Instruction List, IL) geschrieben sind. Bei IL handelt es sich um eine Programmiersprache, die große Ähnlichkeit zu Assembler aufweist.

Ein Hauptproblem beim Model-Checking ist die sogenannte Zustandsraumexplosion. Hierbei wächst die Anzahl der möglichen Systemzustände exponentiell in der Größe der Wertebereiche und der nebenläufigen Programmbestandteile. Statische Analysen betrachten nur den Quelltext eines Programms und skalieren im Gegensatz zum Model-Checking, liefern allerdings in der Regel weniger präzise Ergebnisse als das Model-Checking. Daher werden statische Analysen häufig in Model-Checkern verwendet, um die Zustandsraumexplosion abzumildern.

• R. Huuck, Semantics and Analysis of Instruction List Programs, Proceedings of the Second Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2004). Electronic Notes in Theoretical Computer Science 115, Elsevier, pages 3-18, January 2005.
• B. Schlich, J. Brauer, J. Wernerus, and S. Kowalewski, Direct Model Checking of PLC Programs in IL, in Proceedings of 2nd IFAC Workshop on Dependable Control of Discrete Systems (DCDS 2009), Bari, Italy, 2009, To appear.

Das Ziel der Arbeit ist es, Verfahren zur Bekämpfung der Zustandsraumexplosion zu entwickeln, welche speziell auf PLCs und IL zugeschnitten sind. Darüberhinaus sollen Methoden entwickelt werden, die es erlauben, Fehler in IL-Programmen zu finden ohne den zeitaufwendigen Model-Checking Prozess auszuführen.

• Informatik

• Java
• Eingebette Systeme (hilfreich)

Hier finden sie Hinweise zu Bewerbungen.

• Dr. rer. nat. Jörg Brauer