Optimierung der Verifikation von Correct-by-Construction Produktlinien im Tool VarCorC

  • Kontext: Correctness-by-Construction (CbC) ist ein Verfahren zur Softwareentwicklung. Hierbei werden Programme mit Kontrakten versehen und durch Korrektheit bewahrende Verfeinerungen erstellt. Software Produktlinien (SPLs) werden verwendet, um eine
    Menge von Programmvarianten zu verwalten. Das Tool VarCorC bietet die Möglichkeit, SPLs unter Verwendung von CbC zu entwickeln.

     

    Problem: In VarCorC sind derzeit zwei Ansätze zur Verifikation von Produktlinien implementiert: Ein produkt-basierter und ein familien-basierter Ansatz. In vergleichbaren Verifikationsansätzen sind familien-basierte Ansätze meist effizienter. In einer vorangegangenen Abschlussarbeit wurde evaluiert, dass dies für den implementierten Ansatz in VarCorC nicht der Fall ist. Allerdings war Optimierungspotenzial erkennbar.

     

    Ziel: Untersuchung der Ursachen dafür und Optimierung des bestehenden Ansatzes und Evaluierung der Optimierung.

     

    Voraussetzung: Programmierkenntnisse in Java, Grundlegende Kenntnisse im Bereich der Programmverifikation und -spezifikation