mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
Towards the verification of temporal data consistency in Real-Time Data Management
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-6952-1053
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2898-9570
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
2016 (English)In: 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS, CPS Data 2016, 2016, Article number 7496422Conference paper, Published paper (Refereed)
Resource type
Text
Abstract [en]

Many Cyber-Physical Systems (CPSs) require both timeliness of computation and temporal consistency of their data. Therefore, when using real-time databases in a real-time CPS application, the Real-Time Database Management Systems (RTDBMSs) must ensure both transaction timeliness and temporal data consistency. RTDBMSs prevent unwanted interferences of concurrent transactions via concurrency control, which in turn has a significant impact on the timeliness and temporal consistency of data. Therefore it is important to verify, already at early design stages that these properties are not breached by the concurrency control. However, most often such early on guarantees of properties under concurrency control are missing. In this paper we show how to verify transaction timeliness and temporal data consistency using model checking. We model the transaction work units, the data and the concurrency control mechanism as a network of timed automata, and specify the properties in TCTL. The properties are then checked exhaustively and automatically using the UPPAAL model checker. 

Place, publisher, year, edition, pages
2016. Article number 7496422
Keyword [en]
Complex networks, Embedded systems, Information management, Model checking, Real time systems, Concurrent transactions, Cyber physical systems (CPSs), Early design stages, Real time data management, Real-time database, Real-time database management systems, Temporal consistency, Uppaal model checkers, Concurrency control
National Category
Embedded Systems
Identifiers
URN: urn:nbn:se:mdh:diva-32523DOI: 10.1109/CPSData.2016.7496422ISI: 000390778200005Scopus ID: 2-s2.0-84980619578ISBN: 9781509011544 (print)OAI: oai:DiVA.org:mdh-32523DiVA: diva2:953670
Conference
2nd International Workshop on Modelling, Analysis, and Control of Complex CPS, CPS Data 2016, 11 April 2016
Available from: 2016-08-18 Created: 2016-08-18 Last updated: 2017-05-22Bibliographically approved
In thesis
1. Systematic Design of Data Management for Real-Time Data-Intensive Applications
Open this publication in new window or tab >>Systematic Design of Data Management for Real-Time Data-Intensive Applications
2017 (English)Licentiate thesis, comprehensive summary (Other academic)
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.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2017
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 258
National Category
Computer Systems
Identifiers
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 (English)
Opponent
Supervisors
Projects
DAGGERS
Funder
Knowledge Foundation
Available from: 2017-05-23 Created: 2017-05-22 Last updated: 2017-07-10Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Gallina, BarbaraNyström, DagSeceleanu, Cristina

Search in DiVA

By author/editor
Cai, SiminGallina, BarbaraNyström, DagSeceleanu, Cristina
By organisation
Embedded Systems
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 286 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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