Correctness-by-Construction (CbC)

  • Ansprechperson:

    Tabea Bordis, Maximilian Kodetzki, Rasmus Rønneberg, Ina Schaefer

  • Starttermin:

    Dezember 2017

  • Endtermin:

    Offen

Links

Correctness-by-Construction (CbC) ist ein Ansatz zur inkrementellen Erstellung korrekter Programme. CbC beginnt mit einem abstrakten Hoare-Tripel {P} S {Q}, das aus einer Vorbedingung P, einer abstrakten Anweisung S und einer Nachbedingung Q besteht. Hoare-Tripel stellen vollständige Korrektheitsaussagen dar, die nur dann als wahr bewertet werden, wenn, ausgehend von der Vorbedingung, die Nachbedingung nach Ausführung des schließlich definierten konkreten Programms erfüllt ist. Bei CbC wird das Hoare-Tripel mit Hilfe einer Menge von Verfeinerungsregeln sukzessive zu einer konkreten Implementierung verfeinert, die die Spezifikation erfüllt. Die Korrektheit ist garantiert, da jede Verfeinerungsregel als solide bewiesen ist und die Korrektheit des Programms bewahrt. CbC ist in dem Werkzeug CorC implementiert. CorC ist eine grafische und textuelle IDE zur Konstruktion von Algorithmen nach dem Correctness-by-Construction-Ansatz. Es unterstützt CbC-Entwickler dabei, ein Programm durch eine Abfolge von Verfeinerungsschritten zu verfeinern und die Korrektheit dieser Verfeinerungsschritte mit Hilfe eines Theoremprüfers zu verifizieren.

Informationsflusskontrolle durch Konstruktion

Neben der Verifikation der funktionalen Korrektheit können Verfeinerungsregeln auch zur Gewährleistung der Sicherheit von Programmen eingesetzt werden. Eine Informationsfluss-Policy definiert, wie Informationen in einem Programm fließen dürfen (z.B. ist ein Fluss von öffentlichen zu geheimen Daten erlaubt, aber der andere Weg ist verboten). Die Erweiterung von CbC zur Gewährleistung der Sicherheit wird als Information Flow Control-by-Construction (IFbC) bezeichnet. Programme werden inkrementell unter Verwendung von Verfeinerungsregeln konstruiert, um einer Informationsfluss-Policy zu folgen. In jedem Verfeinerungsschritt wird die Sicherheit und funktionale Korrektheit des Programms garantiert, so dass unsichere Programme durch Konstruktion verhindert werden. Die Informationsfluss-Policy kann in einem beliebigen begrenzten oberen Semilattice spezifiziert werden (d. h. die Sicherheitsstufen sind in einer teilweise geordneten Menge angeordnet, die die zulässige Richtung des Informationsflusses darstellt). IFbC ist in einer Erweiterung von CorC implementiert.

Correctness-by-Construction für Software-Produktlinien

Software-Produktlinien bieten eine systematische Wiederverwendung von Software und anderen Artefakten, gepaart mit Variabilitätsmechanismen im Code, um ganze Produktfamilien und nicht nur einzelne Softwareprodukte zu implementieren. Die Gemeinsamkeiten und Unterschiede der einzelnen Varianten werden als Features kommuniziert, deren Beziehungen oft in Feature-Modellen modelliert werden. Die Gewährleistung der Korrektheit einer Produktlinie ist aufgrund der Anzahl möglicher Varianten, die sich aus der Anzahl der Feature-Konfigurationen und der variablen Codestrukturen ergeben, eine besondere Herausforderung. Um eine korrekte Produktlinie mit CbC zu erstellen, haben wir daher den ursprünglichen CbC-Ansatz um eine neue Verfeinerungsregel für einen Variabilitätsmechanismus in den Aussagen des Hoare-Tripels erweitert und mit einer Vertragskomposition für Variabilität in der Vor- und Nachbedingung kombiniert. Wir nennen diese Erweiterung Variational Correctness-by-Construction. VarCorC verwendet FeatureIDE und variationales CbC, um die Entwicklung von Correctness-by-Construction Software-Produktlinien zu unterstützen.

Publikationen