This lecture teaches the basics and applications of static analysis and model checking in the domain of logic control software. To this end, common analyses and algorithms are applied to the cyclic execution model of programmable logic controllers. Topic are, among others:

• The programming language Structured Text
  • Definition from IEC-61131-3
  • Formalisation as control flow graph
• Static analysis
  • Data flow analysis
    • Order-theoretical foundations (Complete Lattice)
    • Live Variables Analysis
    • Reaching Definitions Analysis
    • Value Set Analysis
  • Program Dependency Graphs
  • Slicing
• Abstract Interpretation
  • Galois Connections
  • 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

• Tuesday 14:30-16:00 AH III
• Friday 10:30-12:00 AH III

There will be voluntary exercise sheets published every week and solved in the exercise class. There will be recordings of the lectures and exercise classes available in the moodle course room.

TBA

https://moodle.rwth-aachen.de/course/view.php?id=36573

• Thomas Henn, M.Sc. RWTH
• Dr. rer. nat. Marcus Völker