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 Kontrollflussautomat
  • Statische Analyse
    • Datenflussanalysen
      • Ordnungstheoretische Grundlagen (Complete Lattice)
      • Live Variables Analysis
      • Reaching Definitions Analysis
      • Value Set Analysis
    • Program Dependency Graphs
    • Slicing
  • Abstract Interpretation
    • Galois-Verbindungen
    • Structural Operational Semantics
    • CEGAR-Variant for PLC State Space exploration
  • Specification and Model Checking
    • LTL
    • Specification Automata
  • Logical Characterisation and Symbolic Reasoning
    • SMT encoding of Structured Text
    • Symbolic Execution
    • Large Block Encoding

Termine

  • Montags 16:30-18:00 im AH IV
  • Dienstags 12:30-14:00 im AH V

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 Moodle angekündigt. Die Vorlesung wird auf Video aufgezeichnet (d.h. Bildschirmaufnahme und Mikrofon), die Übung nicht.

Klausur

Anfang und Ende März, genaue Termine und Modalitäten werden noch bekanntgegeben

Klausurrelevant sind die Inhalte aller Vorlesungen und Übungen.

Moodle

Kontakt

Diese Website verwendet Cookies. Durch die Nutzung der Website stimmen Sie dem Speichern von Cookies auf Ihrem Computer zu. Wenn Sie nicht einverstanden sind, verlassen Sie bitte die Website.Weitere Information

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