mdh.sePublikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A Formal Approach for Flexible Modeling and Analysis of Transaction Timeliness and Isolation
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. IS (Embedded Systems).
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. IS (Embedded Systems).ORCID-id: 0000-0002-6952-1053
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. IS (Embedded Systems).ORCID-id: 0000-0003-2898-9570
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. IS (Embedded Systems).ORCID-id: 0000-0003-2870-2680
2016 (engelsk)Inngår i: Proceedings of the 24th International Conference on Real-Time Networks and Systems, Brest, France, 2016Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

Traditional Concurrency Control (CC) mechanisms ensure absence of undesired interference in transaction-based systems and enforce isolation. However, CC may introduce unpredictable delays that could lead to breached timeliness, which is unwanted for real-time transactions. To avoid deadline misses, some CC algorithms relax isolation in favor of timeliness, whereas others limit possible interleavings by leveraging real-time constraints and preserve isolation. Selecting an appropriate CC algorithm that can guarantee timeliness at an acceptable level of isolation thus becomes an essential concern for system designers. However, trading-off isolation for timeliness is not easy with existing analysis techniques in database and real-time communities. In this paper, we propose to use model checking of a timed automata model of the transaction system, in order to check the traded-off timeliness and isolation. Our solution provides modularization for the basic transactional constituents, which enables flexible modeling and composition of various candidate CC algorithms, and thus reduces the effort of selecting the appropriate CC algorithm.

sted, utgiver, år, opplag, sider
Brest, France, 2016.
Emneord [en]
Transaction management, concurrency control, timeliness, isolation, model checking
HSV kategori
Identifikatorer
URN: urn:nbn:se:mdh:diva-33826DOI: 10.1145/2997465.2997495ISI: 000391255400001Scopus ID: 2-s2.0-84997170469OAI: oai:DiVA.org:mdh-33826DiVA, id: diva2:1048588
Konferanse
24th International Conference on Real-Time Networks and Systems RTNS'16, 19 Oct 2016, Brest, France
Prosjekter
DAGGERS - Data aggregation for embedded real-time database systemsTilgjengelig fra: 2016-11-21 Laget: 2016-11-21 Sist oppdatert: 2019-09-13bibliografisk kontrollert
Inngår i avhandling
1. Systematic Design of Data Management for Real-Time Data-Intensive Applications
Åpne denne publikasjonen i ny fane eller vindu >>Systematic Design of Data Management for Real-Time Data-Intensive Applications
2017 (engelsk)Licentiatavhandling, med artikler (Annet vitenskapelig)
Abstract [en]

Modern real-time data-intensive systems generate large amounts of data that are processed using complex data-related computations such as data aggregation. In order to maintain the consistency of data, such computations must be both logically correct (producing correct and consistent results) and temporally correct (completing before specified deadlines). One solution to ensure logical and temporal correctness is to model these computations as transactions and manage them using a Real-Time Database Management System (RTDBMS). Ideally, depending on the particular system, the transactions are customized with the desired logical and temporal correctness properties, which are achieved by the customized RTDBMS with appropriate run-time mechanisms. However, developing such a data management solution with provided guarantees is not easy, partly due to inadequate support for systematic analysis during the design. Firstly, designers do not have means to identify the characteristics of the computations, especially data aggregation, and to reason about their implications. Design flaws might not be discovered, and thus they may be propagated to the implementation. Secondly, trade-off analysis of conflicting properties, such as conflicts between transaction isolation and temporal correctness, is mainly performed ad-hoc, which increases the risk of unpredictable behavior.

In this thesis, we propose a systematic approach to develop transaction-based data management with data aggregation support for real-time systems. Our approach includes the following contributions: (i) a taxonomy of data aggregation, (ii) a process for customizing transaction models and RTDBMS, and (iii) a pattern-based method of modeling transactions in the timed automata framework, which we show how to verify with respect to transaction isolation and temporal correctness. Our proposed taxonomy of data aggregation processes helps in identifying their common and variable characteristics, based on which their implications can be reasoned about. Our proposed process allows designers to derive transaction models with desired properties for the data-related computations from system requirements, and decide the appropriate run-time mechanisms for the customized RTDBMS to achieve the desired properties. To perform systematic trade-off analysis between transaction isolation and temporal correctness specifically, we propose a method to create formal models of transactions with concurrency control, based on which the isolation and temporal correctness properties can be verified by model checking, using the UPPAAL tool. By applying the proposed approach to the development of an industrial demonstrator, we validate the applicability of our approach.

sted, utgiver, år, opplag, sider
Västerås: Mälardalen University, 2017
Serie
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 258
HSV kategori
Identifikatorer
urn:nbn:se:mdh:diva-35369 (URN)978-91-7485-334-6 (ISBN)
Presentation
2017-06-12, Kappa, Mälardalens högskola, Västerås, 13:30 (engelsk)
Opponent
Veileder
Prosjekter
DAGGERS
Forskningsfinansiär
Knowledge Foundation
Tilgjengelig fra: 2017-05-23 Laget: 2017-05-22 Sist oppdatert: 2017-07-10bibliografisk kontrollert
2. Systematic Design and Analysis of Customized Data Management for Real-Time Database Systems
Åpne denne publikasjonen i ny fane eller vindu >>Systematic Design and Analysis of Customized Data Management for Real-Time Database Systems
2019 (engelsk)Doktoravhandling, med artikler (Annet vitenskapelig)
Abstract [en]

Modern real-time data-intensive systems generate large amounts of data that are processed using complex data-related computations such as data aggregation. In order to maintain logical data consistency and temporal correctness of the computations, one solution is to model the latter as transactions and manage them using a Real-Time Database Management System (RTDBMS). Ideally, depending on the particular system, the transactions are customized with the desired logical and temporal correctness properties, which should be enforced by the customized RTDBMS via appropriate transaction management mechanisms. However, developing such a data management solution with high assurance is not easy, partly due to inadequate support for systematic specification and analysis during the design. Firstly, designers do not have means to identify the characteristics of the computations, especially data aggregation, and to reason about their implications. Design flaws might not be discovered early enough, and thus they may propagate to the implementation. Secondly, meeting more properties simultaneously might not be possible, so trading-off the less critical ones for the critical one, for instance, temporal correctness, is sometimes required. Nevertheless, trade-off analysis of conflicting properties, such as transaction atomicity, isolation and temporal correctness, is mainly performed ad-hoc, which increases the risk of unpredictable behavior.

In this thesis, we address the above problems by showing how to systematically design and provide assurance of transaction-based data management with data aggregation support, customized for real-time systems. We propose a design process as our methodology for the systematic design and analysis of the trade-offs between desired properties, which is facilitated by a series of modeling and analysis techniques. Our design process consists of three major steps as follows: (i) Specifying the data-related computations, as well as the logical data consistency and temporal correctness properties, from system requirements, (ii) Selecting the appropriate transaction models to model the computations, and deciding the corresponding transaction management mechanisms that can guarantee the properties, via formal analysis, and, (iii) Generating the customized RTDBMS with the proved transaction management mechanisms, via configuration or implementation. In order to support the first step of our process, we propose a taxonomy of data aggregation processes for identifying their common and variable characteristics, based on which their inter-dependencies can be captured, and the consequent design implications can be reasoned about. Tool support is provided to check the consistency of the data aggregation design specifications. To specify transaction atomicity, isolation and temporal correctness, as well as the transaction management mechanisms, we also propose a Unified Modeling Language (UML) profile with explicit support for these elements. The second step of our process relies on the systematic analysis of trade-offs between transaction atomicity, isolation and temporal correctness. To achieve this, we propose two formal frameworks for modeling transactions with abort recovery, concurrency control, and scheduling. The first framework UPPCART utilizes timed automata as the underlying formalism, based on which the desired properties can be verified by model checking. The second framework UPPCART-SMC models the system as stochastic timed automata, which allows for probabilistic analysis of the properties for large complex RTDBMS using statistical model checking. The encoding of high-level UTRAN specifications into corresponding formal models is supported by tool automation, which we also propose in this thesis. The applicability and usefulness of our proposed techniques are validated via several industrial use cases focusing on real-time data management.

sted, utgiver, år, opplag, sider
Västerås: Mälardalen University, 2019
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 295
HSV kategori
Forskningsprogram
datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-45211 (URN)978-91-7485-441-1 (ISBN)
Disputas
2019-11-04, Gamma, Mälardalens högskola, Västerås, 13:30 (engelsk)
Opponent
Veileder
Tilgjengelig fra: 2019-09-19 Laget: 2019-09-13 Sist oppdatert: 2019-09-26bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopushttp://dl.acm.org/citation.cfm?id=2997495

Søk i DiVA

Av forfatter/redaktør
Cai, SiminGallina, BarbaraNyström, DagSeceleanu, Cristina
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 47 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf