Titelaufnahme

Titel
User-guided predicate abstraction of TLA+ specifications / von Thanh Hai Tran
VerfasserTran, Thanh Hai
Begutachter / BegutachterinKonnov, Igor
ErschienenWien, 2016
Umfangxvii, 125 Seiten : Illustrationen
HochschulschriftTechnische Universität Wien, Diplomarbeit, 2016
Anmerkung
Zusammenfassung in deutscher Sprache
SpracheEnglisch
DokumenttypDiplomarbeit
Schlagwörter (DE)Verifikation / Prädikatabstraktion / SMT / Modelchecking
Schlagwörter (EN)Verification / predicate abstraction / SMT / Modelchecking
URNurn:nbn:at:at-ubtuw:1-5204 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
User-guided predicate abstraction of TLA+ specifications [1.22 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

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.

Zusammenfassung (Englisch)

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.