User-guided predicate abstraction of TLA+ specifications

Abstract

TLA+ ist eine Sprache zur Spezifikation und Verifikation sequenzieller, nebenläufiger und verteilter Systeme. Sie basiert auf den folgenden beiden mathematischen Konzepten: i. der temporalen Logik der Aktionen (TLA) zur Charakterisierung von dynamischem Systemverhalten, und ii. einer Variante der Zermelo-Fraenkel-Mengenlehre mit Auswahlaxiom (ZFC) zur Beschreibung von Datenstrukturen. Diese mathematischen Aspekte machen TLA+ zu einer einfach verwendbaren und flexiblen Sprache für die Spezifikation verschiedenster Systeme. Außerdem ermöglicht es das solide mathematische Fundament der Sprache, die Korrektheit eines Systems formal zu beweisen. Doch obwohl formale Beweise die verlässlichste Methode zur Korrektheitsüberprüfung von Systemen darstellen, ist es oft schwer, derartige Beweise zu finden. Um die formale Verifikation von TLA+ -Spezifikationen zu automatisieren, wurde deshalb der Modelchecker TLC für TLA+ eingeführt, der sich dadurch auszeichnet, dass er die erreichbaren Zustände explizit aufzählt. TLA+ und TLC werden erfolgreich zur Spezifikation und Überprüfung industriell genutzer Systeme verwendet, jedoch wird die praktische Verwendbarkeit von TLC dadurch eingeschränkt, dass er keine Abstraktionstechniken zur Komplexitätsreduktion von Modellen unterstützt. Aus diesem Grund gilt TLC derzeit als ein Werkzeug, das hauptsächlich zur Erkennung einfacher Fehler in TLA+ -Designs dient. Bei der sogenannten Prädikatabstraktion handelt es sich um eine Technik, welche Software-Modelchecking für Systeme mit großem (auch unendlichem) Zustandsraum ermöglicht, indem sie den Zustandsraum mithilfe intelligenter Methoden verkleinert. Dabei wird, ausgehend von einer Menge von Prädikaten über den Systemvariablen, automatisch ein vereinfachtes abstraktes Modell des ursprünglichen Systems generiert, dessen Prädikatwerte und Transitionsrelationen anschließend, unter Verwendung von SMT-Solvern (satisfiability modulo theories solver), überprüft werden. In dieser Arbeit verbinden wir TLA+ mit benutzergeführter Prädikatabstraktion. Das Hauptziel dieser Arbeit ist die Entwicklung eines neuen Modelcheckers für TLA+-Spezifikationen, der basierend auf einer gegebenen Menge von Prädikaten ein abstraktes Modell erzeugen und verifizieren kann.

TLA+ ist eine Sprache zur Spezifikation und Verifikation sequenzieller, nebenläufiger und verteilter Systeme. Sie basiert auf den folgenden beiden mathematischen Konzepten: i. der temporalen Logik der Aktionen (TLA) zur Charakterisierung von dynamischem Systemverhalten, und ii. einer Variante der Zermelo-Fraenkel-Mengenlehre mit Auswahlaxiom (ZFC) zur Beschreibung von Datenstrukturen. Diese mathematischen Aspekte machen TLA+ zu einer einfach verwendbaren und flexiblen Sprache für die Spezifikation verschiedenster Systeme. Außerdem ermöglicht es das solide mathematische Fundament der Sprache, die Korrektheit eines Systems formal zu beweisen. Doch obwohl formale Beweise die verlässlichste Methode zur Korrektheitsüberprüfung von Systemen darstellen, ist es oft schwer, derartige Beweise zu finden. Um die formale Verifikation von TLA+ -Spezifikationen zu automatisieren, wurde deshalb der Modelchecker TLC für TLA+ eingeführt, der sich dadurch auszeichnet, dass er die erreichbaren Zustände explizit aufzählt. TLA+ und TLC werden erfolgreich zur Spezifikation und Überprüfung industriell genutzer Systeme verwendet, jedoch wird die praktische Verwendbarkeit von TLC dadurch eingeschränkt, dass er keine Abstraktionstechniken zur Komplexitätsreduktion von Modellen unterstützt. Aus diesem Grund gilt TLC derzeit als ein Werkzeug, das hauptsächlich zur Erkennung einfacher Fehler in TLA+ -Designs dient. Bei der sogenannten Prädikatabstraktion handelt es sich um eine Technik, welche Software-Modelchecking für Systeme mit großem (auch unendlichem) Zustandsraum ermöglicht, indem sie den Zustandsraum mithilfe intelligenter Methoden verkleinert. Dabei wird, ausgehend von einer Menge von Prädikaten über den Systemvariablen, automatisch ein vereinfachtes abstraktes Modell des ursprünglichen Systems generiert,