Aufgabenblätter und Organisatorisches · Formale Voraussetzungen

Wintersemester 2016/2017

PSE – Gruppe I

Umsetzung einer Entwicklungsumgebung zur Spezifikation & Verifikation von Software für Produktionsanlagen

Prof. Dr. Bernhard Beckert
Alexander Weigl, Dr. Mattias Ulbrich

Inhalt

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.

Skizze einer Implementierung

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.

Gruppentermine

Abgabe der Artefakten: Jeweils am Montag, 09:00 Uhr vor dem Kolloquium.

Termin Zeit Inhalt Ort
07.11.2016 13:00 Uhr Erstes Gruppentreffen
Kick-Off Folien
Geb. 50.34, Raum 211
16.11.2016 Gruppenteffen
Überblick SPS-Programmierung und Testtabellen
Arbeitsauftrag: Pflichtenheft
Geb. 50.34, Raum 211
23.11.2016 Gruppenteffen Geb. 50.34, Raum 211
30.11.2016 Gruppenteffen Geb. 50.34, Raum 211
07.12.2016 Kolloquium Geb. 50.34, Raum 211
14.12.2016 Gruppenteffen Geb. 50.34, Raum 211
21.12.2016 Gruppenteffen Geb. 50.34, Raum 211
11.01.2017 Gruppenteffen Geb. 50.34, Raum 211
18.01.2017 Gruppenteffen Geb. 50.34, Raum 211
25.01.2017 Kolloquium Geb. 50.34, Raum 211
01.02.2017 Gruppenteffen Geb. 50.34, Raum 211
08.02.2017 Gruppenteffen Geb. 50.34, Raum 211
15.02.2017 Gruppenteffen Geb. 50.34, Raum 211
22.02.2017 Kolloquium Geb. 50.34, Raum 211
01.03.2017 Gruppenteffen Geb. 50.34, Raum 211
08.03.2017 Gruppenteffen Geb. 50.34, Raum 211
15.03.2017 Kolloquium Geb. 50.34, Raum 211
KW 12 2017 Abschlusspräsentation Geb. 50.34

Weitereführende Informationen

  • PPU
  • Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl: “Regression Verification for Programmable Logic Controller Software”, 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings, LNCS 9407, 2015. Seiten 234-251