ICT Call 2015 / ICT15-103
Igor Konnov  Josef Widder
Principal Investigator:
Igor Konnov Personal webpage
Institution:
Vienna University of Technology Webpage
Projekttitel:
APALACHE: Abstraction-based Parameterized TLA Checker Project Webpage
ProjektpartnerInnen:
Josef Widder (Vienna University of Technology) (Co-Principal Investigator) Personal webpage
Status:
Laufend (01.01.2016 – 31.12.2018) 36 Monate
Fördersumme:
€ 539.000

 
Kurzzusammenfassung:

Moderne Internetdienste, wie die von Amazon, Google, Facebook, oder Netflix, laufen in der Cloud.
Benutzeranfragen werden von zehntausenden Computern bearbeitet, die sich in weltweit verteilten Datenzentren befinden. Bei so vielen involvierten Computern werden Fehler von der Ausnahme zur Regel.
Daher wird es immer wichtiger Fehlertoleranzmechanismen auf rigorose Art zu entwerfen und zu verifizieren, dass diese Mechanismen tatsächlich ihre Aufgaben erfüllen.
TLA+ ist ein Formalismus, den Turing-Preisträger Leslie Lamport erfunden hat, um solche Fehlertoleranzmechanismen zu entwerfen. Das APALACHE Projekt widmet sich automatischen Verifikationsmethoden für TLA+. Wir entwickeln ein Model-Checking-Programm namens Apalache, das modernste automatische Verifikationsmethoden auf TLA+ anwendet. In späteren Projektphasen werden wir Apalache mit neu-entwickelten parameterisierten Model-Checking-Methoden erweitern um automatische Verifikation großer Systeme zu ermöglichen.

 

Diese Seite verwendet Cookies. Durch das Nutzen dieser Seite sind Sie mit der Verwendung von Cookies einverstanden. Details finden Sie hier.