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
  • 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

The digital exercise class will take place every Friday from 10:30-12:00 via Zoom. See moodle for the link.

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

TBA

The contents of all lectures and exercise sheets will be relevant for the exam.

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

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