Institute of Computer Science

LTG

Theses

Analyse des MVCC Mechanismus von PostgreSQL

Multi-version concurrency control (MVCC) bezeichnet ein System zur Implementatierung der Transaktionskontrolle in Datenbanken. Ziele dieser Arbeit sind:

1. MVCC in PostgreSQL in allen Details verstehen;

2. eine Modallogik entwickeln, um MVCC formal präzise zu modellieren;

3. mit Hilfe dieser Logik einige Eigenschaften von MVCC verifizieren.

 

PCTL mit nicht-standard Wahrscheinlichkeiten

Computation Tree Logic (CTL) ist eine Logik, die speziell zur Verifikation von Hardware und Software dient. Probabilistisches CTL (PCTL) bezeichnet eine Erweiterung von CTL mit Wahrscheinlichkeitsquantoren. Damit kann bspw. ausgedrückt werden, dass eine Anfrage mit 98% Wahrscheinlichkeit innerhalb von 2 Sekunden beantwortet wird. Jedoch gibt es auch einige Aussagen, welche man in PCTL nicht formulieren kann. In dieser Arbeit geht es darum, eine Variante von PCTL zu entwickeln, in welcher diese Aussagen möglich sind. Dazu sollen nicht-standard Wahrscheinlichkeiten verwendet werden. Ausserdem soll gezeigt werden, dass das Model Checking Problem für nicht-standard PCTL entscheidbar ist.

 

Sequenzenkalkül für Macaroons

Macaroons bilden einen flexiblen Autorisierungsmechanismus für dezentralisierte verteilte Systeme. Um die Eigenschaften von Macaroons formal zu beschrieben, gibt es bereits eine erweitere Autorisierungslogik. Allerdings ist diese Logik ungeeignet für automatische Beweissuche und deren Implementierungen.
Ziel dieser Arbeit ist es, einen Sequenzenkalkül für diese Autorisierungslogik zu entwickeln, welcher automatische Beweissuche unterstützt.



Weitere Themen aus dem Bereich Logik und theoretische Informatik sind möglich. Falls Sie ein Thema für eine Arbeit vorschlagen möchten, nehmen Sie bitte mit uns Kontakt auf.