PSE – Gruppe I

Hintergrund

Im Zeitalter von Industrie 4.0 sollen Industrieanlagen individuell konfigurierte Produkte vollautomatisch und autonom herstellen können. Diese Anforderung lässt die Software in Anlagensteuerungen zunehmend komplexer werden. Dennoch muss sie Sicherheitsaspekte, wie zum Beispiel das korrekte Verhalten im Falle eines Nothalts, gewährleisten, um Leib und Leben der Angestellten zu schützen. Formale Verifikation kann hier eingesetzt werden, um bereits während der Entwicklung zu beweisen, dass Software definierte Sicherheitsspezifikationen einhält.

Automatisierungssteuerungen sind reaktive Systeme, die in zyklischen Abständen Sensorwerte einlesen und Aktuatorwerte berechnen. Daher müssen Sicherheitsspezifikationen auch über Abfolgen von Ein- und Ausgaben formuliert werden, was ihren Umfang und ihre Komplexität erhöht und damit ihre Verständlichkeit verringert.

Aufgabenbeschreibung

In diesem PSE-Projekt soll eine grafische Entwicklungsumgebung entwickelt werden, die dem Automatisierungsingenieur dabei helfen soll, das funktionale Verhalten von Anlagensoftware zu spezifizieren, zu verifizieren und Fehler (in Form von Gegenbeispiele) zu verstehen.

Die Entwicklungsumgebung soll mindestens folgende Komponenten umfassen:

1. Einen Code-Editor für die Programmierung in der Programmiersprache Structured Text.
2. Eine tabellarische Darstellung der Spezifikation, die auch Bearbeitung zulässt.
3. Eine grafische Ansicht der Spezifikation als Timing-Diagramm.
4. Timing-Diagramme sollen auch als Visualisierung der Gegenbeispiele dienen.

Die Software soll möglichst robust gegen fehlerhafte und unerwartete Eingaben sein. So sollen z. B. zyklische Referenzen oder unerfüllbare Bedingungen durch Ihr System abgefangen werden, damit der Benutzer frühzeitig auf potentielle Probleme hingewiesen wird.

Die Umsetzung soll in der Programmiersprache Java erfolgen. Eine Schnittstelle zum Verifikationssystem wird bereitgestellt.

Anforderungen

Bei diesen Thema werden Sie mit Techniken der statischer Analyse von Programmen und der formaler Verifikation in Berührung kommen. Wenngleich es nicht notwendig ist, tief in diese Felder einzutauchen, erwarten wir Ihre Bereitschaft, sich mit diesen spannenden Themen ein wenig auseinanderzusetzen.

Die Softwareentwicklung soll nach den aktuellen Best-Practises umgesetzt werden unter Einsatz von

• Source Code Management,
• automatischen Build-Tools,
• automatischem Testen,
• Continuous Integration,
• Style Checkers und
• Design Patterns.

Dieses PSE-Projekt ist Teil des Forschungsprojekts IMPROVE APS. Eine Projektvorstellung für unsere Projektpartner an der TU München ist geplant, nach Möglichkeit mit einer Evaluierung der Gebrauchstauglichkeit und Verständlichkeit des entwickelten Produkts.