The public defense of Simin Cai's doctoral thesis in Computer Science

Doctoral thesis and Licentiate seminars

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

The public defense of Simin Cai´s doctoral thesis in Computer Science will take place at Mälardalen University, room Gamma, MDH Västerås, at 13.30 on November 4, 2019.

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

Serial number: 295

The faculty examiner is Professor Marieke Huisman, University of Twente.

The examining committee consists of Associate Professor Enrico Bini, Universita degli Studi di Torino, Associate Professor Dragoᶊ Truᶊcan, Åbo akademi, Professor Magnus Jonsson, Halmstad University 

Reserve: Professor Thomas Nolte, Mälardalen University


Many modern software systems, ranging from an SMS app in a cellphone with a few texts to a banking system with millions of accounts, use databases to store their information. Usually, all accesses and modifications of the information in a database is performed through a DataBase Management System (DBMS). One major goal of the DBMS is to ensure that the information contained in the database is logically correct, even when the database is accessed by a number of users at the same time, or under failures such as power losses. Various mechanisms are applied by DBMSs to maintain the correctness. As an example, consider two users simultaneously editing a Wiki page whose texts are stored in a database. Without proper synchronization, a sentence can be modified arbitrarily, which as a result may become a meaningless mixture of crumbled words from both users. To avoid this, a DBMS applies concurrency control to order the modifications so that the changes appear to occur one after the other, and the logical correctness of the texts is ensured. Furthermore, recovery techniques are adopted by a DBMS to restore the correct data when unexpected failure occurs. An example is to recover the correct account balance in a bank system when a transaction is canceled due to interrupted connection.

In a type of systems called real-time systems, the work performed by the software need to complete before a given deadline, in order to fulfil a functionality or avoid a failure. For instance, the airbag in a car must inflate before a deadline when an accident occurs. Failing to meet this deadline may cause loss of lives. If such work involves interaction with the database, this interaction also naturally needs to finish in time. To achieve this, the DBMS, which manages database access and modification, must guarantee timely behaviors of these interactions. This type of DBMSs is called Real-Time DBMSs (RTDBMSs).

Therefore, an RTDBMS must satisfy two properties: the logical correctness under various interactions and possible failures, and the temporal correctness of the interactions. A challenge to RTDBMS design is that, there exists a large number of mechanisms to construct an RTDBMS, each having a different effect on the logical and temporal correctness. In particular, many mechanisms for ensuring logical correctness could introduce arbitrary delays that harm temporal correctness. Such issues give rise to questions like: Which mechanisms should the designer select in order to ensure both properties? Moreover, in case that both properties cannot be guaranteed at the same time, how can the designer relax the guarantee to a less strict but still acceptable level, and come up with a feasible RTDBMS design?

In this thesis, Simin Cai investigates how to address these questions in a systematic way. He presents an approach to analyze the RTDBMS interactions, and model the RTDBMS interactions together with various mechanisms mathematically. Based on the models, one can use a well-established tool called UPPAAL to analyze the logical correctness and timeliness of the interactions prior to implementation. By applying this approach, an RTDBMS designer can decide the appropriate mechanisms that satisfy the desired properties, and use them to create an applicable RTDBMS solution.