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 graph
  • Static analysis
    • Data flow analysis
      • Order-theoretical foundations (Complete Lattice)
      • Live Variables Analysis
      • Reaching Definitions Analysis
      • Value Set Analysis
    • Program Dependency Graphs
    • Slicing
    • Policy Iteration
  • 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

Dates

The regular lecture and exercise dates are on Monday and Wednesday 10:30-12:00 in lecture hall AH II, starting on October 8th. More information can be found in the L2P course room

Lecture and exercise class

There will be voluntary exercise sheets published every week and solved in the exercise class. The lecture will be recorded on video (i.e. screen recording and microphone). The exercise class will not be recorded.

Exam

The first exam will be on February 4th at 10:30 (AH I, AH III, BS I)– the second exam on March 6th at 10:30 (AH II, AH III).

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

L2P

Contact


RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany