mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Formal Approach for Flexible Modeling and Analysis of Transaction Timeliness and Isolation
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).ORCID iD: 0000-0002-6952-1053
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).ORCID iD: 0000-0003-2898-9570
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. IS (Embedded Systems).ORCID iD: 0000-0003-2870-2680
2016 (English)In: Proceedings of the 24th International Conference on Real-Time Networks and Systems, Brest, France, 2016Conference paper (Refereed)
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.

Place, publisher, year, edition, pages
Brest, France, 2016.
Keyword [en]
Transaction management, concurrency control, timeliness, isolation, model checking
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:mdh:diva-33826DOI: 10.1145/2997465.2997495ISI: 000391255400001ScopusID: 2-s2.0-84997170469OAI: oai:DiVA.org:mdh-33826DiVA: diva2:1048588
Conference
24th International Conference on Real-Time Networks and Systems RTNS'16, 19 Oct 2016, Brest, France
Projects
DAGGERS - Data aggregation for embedded real-time database systems
Available from: 2016-11-21 Created: 2016-11-21 Last updated: 2017-02-02Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopushttp://dl.acm.org/citation.cfm?id=2997495

Search in DiVA

By author/editor
Cai, SiminGallina, BarbaraNyström, DagSeceleanu, Cristina
By organisation
Embedded Systems
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 4 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf