Tool Supported Specification and Verification of Highly Available Applications

  • Today, information systems are often distributed to achieve high availability and low latency. These systems can be realized by building on a highly available database to manage the distribution of data. However, it is well known that high availability and low latency are not compatible with strong consistency guarantees. For application developers, the lack of strong consistency on the database layer can make it difficult to reason about their programs and ensure that applications work as intended. We address this problem from the perspective of formal verification. We present a specification technique, which allows specifying functional properties of the application. In addition to data invariants, we support history properties. These let us express relations between events, including invocations of the application API and operations on the database. To address the verification problem, we have developed a proof technique that handles concurrency using invariants and thereby reduces the problem to sequential verification. The underlying system semantics, technique and its soundness proof are all formalized in the interactive theorem prover Isabelle/HOL. Additionally, we have developed a tool named Repliss which uses the proof technique to enable partially automated verification and testing of applications. For verification, Repliss generates verification conditions via symbolic execution and then uses an SMT solver to discharge them.
  • Informationssysteme werden mittlerweile oft als verteilte Systeme gebaut, um hohe Verfügbarkeit und geringe Latenz zu erreichen. Zur Realisierung solcher Systeme kann auf hochverfügbare Datenbanken zurückgegriffen werden, welche die Verteilung der Daten übernehmen. Allerdings ist auch bekannt, dass hohe Verfügbarkeit und geringe Latenz nicht kompatibel mit starken Garantien bezüglich Datenkonsistenz sind. Für Anwendungsentwickler kann dieser Verzicht auf starke Konsistenz es erschweren, alle Vorgänge im System präzise zu verstehen und somit sicherzustellen, dass Anwendungen wie gewünscht arbeiten. Wir gehen dieses Problem von der Seite der formalen Verifikation von Software an. Dazu stellen wir eine Spezifikationstechnik vor, die es erlaubt, funktionale Eigenschaften einer Anwendung zu spezifizieren. Neben Invarianten auf den Daten, unterstützt diese Technik auch die Formulierung von History-Eigenschaften. Diese ermöglichen es, bestimmte Ereignisse aus dem Ausführungsverlauf einer Anwendung miteinander in Bezug zu bringen. Zu den Ereignissen gehören Aufrufe der Anwendungsschnittstelle und Operationen, die auf der Datenbank ausgeführt wurden. Um das Verifikationsproblem zu lösen, haben wir eine spezielle Beweistechnik entwickelt, welche den Aspekt der Nebenläufigkeit mithilfe von Invarianten behandelt und damit das Problem auf den sequentiellen Fall reduziert. Die zugrundeliegende Semantik des Systems, die Beweistechnik und der Beweis dessen Korrektheit sind im interaktivem Theorembeweiser Isabelle/HOL formalisiert. Des Weiteren haben wir ein Programmierwerkzeug namens Repliss entwickelt, welches die Beweistechnik verwendet, um die Verifikation und das Testen von Anwendungen teilweise zu automatisieren. Zur Verifikation verwenden wir eine Form der symbolischen Auswertung, welche mathematische Beweisverpflichtungen erzeugt, die dann durch einen SMT-Solver bewiesen werden können.

Download full text files

Export metadata

Metadaten
Author:Peter ZellerORCiD
URN:urn:nbn:de:hbz:386-kluedo-65755
DOI:https://doi.org/10.26204/KLUEDO/6575
Advisor:Arnd Poetzsch-Heffter
Document Type:Doctoral Thesis
Language of publication:English
Date of Publication (online):2021/09/19
Year of first Publication:2021
Publishing Institution:Technische Universität Kaiserslautern
Granting Institution:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2020/11/27
Date of the Publication (Server):2021/09/20
Page Number:XIII, 194
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
CCS-Classification (computer science):F. Theory of Computation / F.3 LOGICS AND MEANINGS OF PROGRAMS / F.3.1 Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1) / Mechanical verification
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Creative Commons 4.0 - Namensnennung (CC BY 4.0)