Institute of Computer Science

LTG

Student Projects

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.