mdh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat 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 (Engelska)Ingår i: 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 2018Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
2018.
Nationell ämneskategori
Teknik och teknologier Datorsystem
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
Konferens
The 23rd IEEE Pacific Rim International Symposium on Dependable Computing PRDC 2018, 04 Dec 2018, Taipei, Taiwan
Projekt
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)Tillgänglig från: 2018-12-18 Skapad: 2018-12-18 Senast uppdaterad: 2020-02-19Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Personposter BETA

Cai, SiminGallina, BarbaraNyström, DagSeceleanu, Cristina

Sök vidare i DiVA

Av författaren/redaktören
Cai, SiminGallina, BarbaraNyström, DagSeceleanu, Cristina
Av organisationen
Inbyggda system
Teknik och teknologierDatorsystem

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 36 träffar
RefereraExporteraLänk till posten
Permanent länk

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