|Forschungsthema:||Improve APS, PLC Verification|
|Typ:||MA / PdF|
Since 2007, IC3 and property-directed reachability (PDR) became de-facto standard in the domain of symbolic model checking. Both approaches are decision procedures to verify that an given invariant is hold by the modelled system. With Regression Verification we can ensure functional equivalence of systems (w.r.t. intended changes). In our case we apply the Regression Verification in the field automated production system to ensure the ensure the well-functioning during the software evolution.
The goal of this thesis is the transfer of the current PDR/IC3 approaches for software model checking to outperform the default implementation on regression verification. The idea is to exploit the main assumption behind regression verification: both software version have an high degree of similar structures. As a benchmark scenario we use the Pick-and-Place-Unit from TUM.
Your task is to understand the current the State-of-the-Art of PDR and IC3; Adapt the ideas into a novel approach, and perform the benchmarks.
Programming skills on C/C++ and Java required. Furthermore, you should be interested in programming languages and SAT solving. You should have completed the Formal Methods (Formale Systeme) Course at KIT or equivalent.