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
Specification and Formal Verification of Atomic Concurrent Real-Time Transactions
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.ORCID-id: 0000-0002-6952-1053
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.ORCID-id: 0000-0003-2898-9570
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.ORCID-id: 0000-0003-2870-2680
2018 (engelsk)Inngår i: 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 2018Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

Although atomicity, isolation and temporal correctness are crucial to the dependability of many real-time database-centric systems, the selected assurance mechanism for one property may breach another. Trading off these properties requires to specify and analyze their dependencies, together with the selected supporting mechanisms (abort recovery, concurrency control, and scheduling), which is still insufficiently supported. In this paper, we propose a UML profile, called UTRAN, for specifying atomic concurrent real-time transactions, with explicit support for all three properties and their supporting mechanisms. We also propose a pattern-based modeling framework, called UPPCART, to formalize the transactions and the mechanisms specified in UTRAN, as UPPAAL timed automata. Various mechanisms can be modeled flexibly using our reusable patterns, after which the desired properties can be verified by the UPPAAL model checker. Our techniques facilitate systematic analysis of atomicity, isolation and temporal correctness trade-offs with guarantee, thus contributing to a dependable real-time database system.

sted, utgiver, år, opplag, sider
2018.
HSV kategori
Identifikatorer
URN: urn:nbn:se:mdh:diva-41710DOI: 10.1109/PRDC.2018.00021ISI: 000462280800012ISBN: 9781538657003 (tryckt)OAI: oai:DiVA.org:mdh-41710DiVA, id: diva2:1272146
Konferanse
The 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 04 Dec 2018, Taipei, Taiwan
Prosjekter
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)Tilgjengelig fra: 2018-12-18 Laget: 2018-12-18 Sist oppdatert: 2020-02-19bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekst

Personposter BETA

Cai, SiminGallina, BarbaraNyström, DagSeceleanu, Cristina

Søk i DiVA

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

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 36 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