Bachelor and Master Theses

Title: Master/Magister thesis: Model-checking transaction properties for concurrent real-time transactions in UPPAAL
Subject: Computer Science
Level: Advanced
Description: Traditionally, a Database Management System (DBMS) maintains data consistency by ensuring the Atomicity, Consistency, Isolation and Durability (ACID) properties during transaction execution. In real-time systems, however, ensuring full ACID may not be desirable or possible, since transactions need to complete before their deadlines. Therefore, in real-time database management systems (RTDBMSs), ACID properties are often relaxed in favor of the timeliness of transactions. A systematic method to compute the trade-offs between ACID and timeliness is needed for developing the transaction management mechanism.
This thesis is intended for Master/Magister students in Intelligent Embedded Systems. The work of this thesis will be part of the DAGGERS research project. The goal of this thesis is as follows:

  • to model the transaction with associated concurrency control mechanisms (e.g. two phase locking, OCC, OCC-TI) in UPPAAL;

  • to specify formally the requirements of the created model as TCTL properties, by applying specification patterns for transformation;

  • to simulate and model-check the resulting model against the formalized requirements;

  • to produce a report describing the method, model and model-checking results.

[1] T. Wang, J. Vonk, B. Kratz, and P. Grefen, “A survey on the history of transaction management: from flat to grid transactions,” Distributed and Parallel Databases, vol. 23, no. 3, pp. 235-270, 2008.
[2] P. S. Yu, K.-L. Wu, K.-J. Lin, and S. H. Son, “On real-time databases: Concurrency control and scheduling,” Proceedings of the IEEE, vol. 82, no. 1, pp. 140-157, 1994.
[3] K. G. Larsen, P. Pettersson, and Y. Wang, “Uppaal in a nutshell,” International Journal on Software Tools for Technology Transfer (STTT), vol. 1, no. 1, pp. 134-152, 1997.
[4] B. Gallina, N. Guelfi, P. Kelsen. Towards an Alloy Formal Model for Flexible Advanced Transactional Model Development. Post-proceedings of the 33rd IEEE Software Engineering Workshop (SEW-33), IEEE Computer Society, ISBN 978-1-4244-6863-8, Skövde (Sweden), 2009.
[5] DAGGERS - Data aggregation for embedded real-time database systems,
Prel. end date: 2016-06-10
Presentation date: 2016-06-02
Student: Jinle Li
IDT supervisor: Simin Cai,
Examinator: Cristina Seceleanu
Cristina Seceleanu, +46-21-151764

Rapport och bilagor


Senaste uppdatering



2016-06-09, 02:34

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2017.08.23