Formale Methoden für Steuerungssoftware

Inhalt

In dieser Vorlesung werden Grundlagen und Anwendungen von statischer Analyse und Model-Checking im Bereich Steuerungssoftware vermittelt. Dazu werden entsprechende Analysen und Algorithmen auf den zyklischen Betrieb von Speicherprogrammierbaren Steuerungen angepasst. Behandelte Themen sind u.A.:

  • Die Programmiersprache Structured Text
    • Definition nach IEC-61131-3
    • Formalisierung als Kontrollflussgraph
  • Statische Analyse
    • Datenflussanalysen
      • Ordnungstheoretische Grundlagen (Complete Lattice)
      • Live Variables Analysis
      • Reaching Definitions Analysis
      • Value Set Analysis
    • Program Dependency Graphs
    • Slicing
    • Policy Iteration
  • Abstract Interpretation
    • Galois-Verbindungen
    • Structural Operational Semantics
    • CEGAR-Variant for PLC State Space exploration
    • Relational Domains
  • Specification and Model Checking
    • CTL
    • Specification Automata
  • Logical Characterisation and Symbolic Reasoning
    • SMT encoding of Structured Text
    • Symbolic Execution
    • Large Block Encoding
    • Bounded Model Checking
    • IC3/PDR

Termine

Die regelmäßigen Veranstaltungstermine sind ab dem 08.10. immer Montag, von 10:30-12:00 im Hörsaal AH II, und Mittwoch, von 10:30-12:00 im Hörsaal AH II, im Hauptbau des Informatikgebäudes. Weitere Informationen werden im L2P und im ersten Vorlesungstermin veröffentlicht.

Vorlesungs- und Übungsbetrieb

Es werden regelmäßig Übungsblätter veröffentlicht und in den Übungen in Zusammenarbeit mit den Studierenden gelöst. Die Übungen finden ebenfalls in den unter 'Termine' genannten Slots statt und werden rechtzeitig in der Vorlesung und im L2P angekündigt. Die Vorlesung wird auf Video aufgezeichnet (d.h. Bildschirmaufnahme und Mikrofon), die Übung nicht.

Klausur

Die erste Klausur findet voraussichtlich am 07.02.2019 statt – die Nachholklausur am 05.03.2019. Die genauen Daten und Räume werden noch bekannt gegeben.

Klausurrelevant sind die Inhalte aller Vorlesungen und Übungen.

L2P

Lernraum wird so bald wie möglich bekanntgegeben.

Kontakt


RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland