Formal Modelling and Analysis of Embedded Systems
DAGGERS - Data aggregation for embedded real-time database systems
In this project, we propose a formal approach where we use product-line methods to engineer a flexible transaction model and the corresponding transaction engine adequate with respect to the temporal and logical consistency requirements.
Project manager at MDH
Description of the project
Embedded real-time systems are currently undergoing a fundamental change. Traditionally these systems have been developed as closed monolithic system with limited interaction with other embedded systems. But recent advances in communications, such as global mobile telecommunication Internet services, have led to that embedded real-time (RT) systems are becoming increasingly interconnected. Thus, these systems are growing more and more complex, and the amount of information that needs to be managed is also rapidly increasing. Therefore, the need for proper RT data management solutions is urgent. System engineers are already faced with difficulties with respect to data aggregation and observability where data can be analysed and acted upon directly during run-time instead of afterwards using off- line tools.
The introduction of database (DB) management systems within RT systems poses an additional challenge since DB transactions not only need to be logically consistent but also temporally consistent (i.e. they have to guarantee timeliness), i.e., DB data must be fresh and transactions must meet their deadlines. To guarantee timeliness, RT transaction models most often relax logical consistency (i.e., by relaxing ACID properties), e.g., by allowing transactions to read uncommitted data or to commit data that is in conflict with some other transaction. Concerning relaxation of I (Isolation), for instance, several notions have been explored and a plethora of RT concurrency- control algorithms has been presented over the years to offer design solutions for those new notions. However, most of these approaches assume a “one size fits all” approach and thus they do not offer the needed flexibility to address different types of transactions.
In this project, we propose a formal approach where we use product-line methods to engineer a flexible transaction model and the corresponding transaction engine adequate with respect to the temporal and logical consistency requirements. Our approach consists in the creation of a formal model of the behavior of the transactions in the system and in the application of verification and validation techniques to (i) verify that all transactions will consistently adhere to the transaction model and to the customer requirements, and (ii) identify all possible transaction conflicts not only based on the write and read set, but based on all possible interleavings of their execution. When all criteria are met, suitable conflict resolution mechanisms, such as RT DB locks, wait-free/lock-free algorithms and temporal isolation, are generated for the particular system.
Our approach enables the introduction of advanced transactions to support data aggregation and management for hard RT embedded systems with maintained predictability and a controlled relaxation of logical consistency.