====== Formal Methods for Logic Control Software ======


=== Content ===

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 automaton
  * 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
    * Bounded Model Checking
  * PLC-specific modeling
    * Instruction List
    * Sequential Function Charts
    * Plant Models
    * Timers

=== Dates ===

The lecture and exercise will take place on Mondays at 16:30 in AH IV and Tuesdays at 12:30 in AH V

=== Lecture and exercise class===

There will be voluntary exercise sheets published every week and solved in the exercise class. 
There will be recordings of the lectures and exercise class available in the moodle course room. We still suggest regular attendance

=== Exam ===

There will be two periods for oral exams in February and March

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

=== moodle ===

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

=== Contact ===

  * [[:lehrstuhl:mitarbeiter:henn]] 
  * [[:lehrstuhl:mitarbeiter:voelker]]