Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Property-Directed Reachability for Regression Verification

Forschungsthema:Improve APS, PLC Verification
Typ: MA / PdF
Datum: 2018-03-01
Betreuer: Alexander Weigl
Bearbeiter:
Aushang:

Background

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.

Goal

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.

Task

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.

Your profile

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.

References

  1. Aaron R. Bradley. SAT-based Model Checking Without Unrolling. VMCAI 2011.
  2. Alessandro Cimatti and Alberto Griggio. Software model Checking via IC3. CAV 2012.
  3. Tim Lange, Martin R. Neuhäußer, and Thomas Noll. IC3 Software Model checking on control flow automata. FMCAD 2015.