Simin Cai försvarar sin doktorsavhandling i datavetenskap

Disputationer och licentiatseminarier

Datum: 2019-11-04
Tid: 13.30
Plats: sal Gamma, MDH Västerås.

Simin Cai, vid akademin för innovation, design och teknik (IDT), försvarar sin doktorsavhandling i datavetenskap, den 4 november, klockan 13.30 i sal Gamma, MDH Västerås.

Titel: “Systematic Design and Analysis of Customized Data Management for Real-Time Database Systems”.
 

Serienummer: 295

Opponent är professor Marieke Huisman, University of Twente.

Betygsnämnden utgörs av docent Enrico Bini, Universita degli Studi di Torino, docent Dragoᶊ Truᶊcan, Åbo akademi, professor Magnus Jonsson, Högskolan i Halmstad. 

Reserv är professor Thomas Nolte , MDH.

 

Sammanfattning:

Många moderna mjukvarusystem, från SMS-applikationer i mobiltelefoner till banksystem med milliontals konton, använder databaser för att lagra sin information. Vanligtvis utförs läsningar och modifieringar av informationen i databasen genom ett databashanteringssystem (DataBase Management System - DBMS). Ett av de grundläggande syftena med en DBMS är att se till att informationen i databasen är logiskt korrekt, även om databasen används av flera användare på samma gång, eller efter systemfel, såsom strömavbrott. Ett flertal mekanismer i DBMSn krävs för att upprätthålla informationens korrekthet. Till exempel, anta att två användare samtidigt uppdaterar en Wiki sida, där texten lagras i en databas. Utan tillräcklig synkronisering uppdateras texten godtyckligt vilket kan leda till meningslösa meningar bestående en blandning av ord från båda användarna. För att undvika detta använder databaser samtidighetskontroll för att ordna modifieringarna så att ändringarna verkar ha hänt efter varandra så att den logiska korrektheten bibehålls. Vidare används återhämtningstekniker i DBMSn för att återskapa data efter oväntade systemfel. Ett exempel är att man återskapar de korrekta saldona i ett banksystem när en överföring avbryts på grund av förlorad uppkoppling mot banken.

I en specifik typ av mjukvarusystem, realtidsystem, måste dessutom arbete fullföljas inom givna tidsramar för att undvika fel. Ta till exempel en airbag i en bil, där denna måste blåsas upp inom en given tid när en olycka sker. Om systemet misslyckas med detta kan det innebära risk för liv. Om detta arbete innefattar operationer till databasen måste givetvis databasen också fullfölja dessa i tid. För att uppnå detta i DBMSn, som ju hanterar läsningar och modifieringar, måste denna kunna garantera ett givet tidsbeteende. Denna typ av DBMS kallas för realtidsdatabashanterare (RTDBMS).

En RTDBMS måste sålunda uppfylla två egenskaper, logisk korrekthet, även vid eventuella systemfel, samt temporal korrekthet för operationer. En utmaning för designen av en RTDBMS är att dessa består av hundratals mekanismer som var och en påverkar den logiska och temporala korrektheten. Vidare så har många av mekanismerna för att upprätthålla den logiska korrektheten en negativ inverkan på den temporala korrektheten genom att de introducerar godtyckligt tidsbeteende. Frågan som då uppstår blir: Vilka mekanismer, för ett givet system, skall en designer välja för att tillfredsställa båda kraven? Och i de fallen båda kraven inte kan garanteras: Hur kan man släppa på dessa garantier men fortsatt hålla dessa på en acceptabel nivå för att kunna ta fram en tillfredställande RTDBMS design?

I den här avhandlingen, undersöker Simin Cai hur man kan svara på ovanstående frågor på ett systematiskt sätt. Han presenterar en metod för att analysera interaktionerna i RTDBMSn, för att sedan modellera dessa i ett välkänt modelleringsverktyg, UPPAAL, så att de kan analyseras med avseende på logisk och temporal korrekthet. Genom att använda denna metod kan en RTDBMS designer välja lämpliga mekanismer för att uppfylla de önskade egenskaperna och använda dessa för att skapa en tillämplig RTDBMS.