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
Systematic Design and Analysis of Customized Data Management for Real-Time Database Systems
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (Formal Modelling and Analysis of Embedded Systems)
2019 (English)Doctoral 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 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.

Place, publisher, year, edition, pages
Västerås: Mälardalen University , 2019.
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 295
National Category
Software Engineering
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-45211ISBN: 978-91-7485-441-1 (print)OAI: oai:DiVA.org:mdh-45211DiVA, id: diva2:1351297
Public defence
2019-11-04, Gamma, Mälardalens högskola, Västerås, 13:30 (English)
Opponent
Supervisors
Available from: 2019-09-19 Created: 2019-09-13 Last updated: 2019-09-26Bibliographically approved
List of papers
1. Data Aggregation Processes: A Survey, A Taxonomy, and Design Guidelines
Open this publication in new window or tab >>Data Aggregation Processes: A Survey, A Taxonomy, and Design Guidelines
2019 (English)In: Computing, ISSN 0010-485X, E-ISSN 1436-5057, Vol. 101, no 10, p. 1397-1429Article in journal (Refereed) Published
Abstract [en]

Data aggregation processes are essential constituents for data management in modern computer systems, such as decision support systems and Internet of Things (IoT) systems, many with timing constraints. Understanding the common and variable features of data aggregation processes, especially their implications to the timerelated properties, is key to improving the quality of the designed system and reduce design effort. In this paper, we present a survey of data aggregation processes in a variety of application domains from literature.We investigate their common and variable features, which serves as the basis of our previously proposed taxonomy called DAGGTAX. By studying the implications of the DAGGTAX features, we formulate a set of constraints to be satisfied during design, which helps to check the correctness of the specifications and reduce the design space. We also provide a set of design heuristics that could help designers to decide the appropriate mechanisms for achieving the selected features. We apply DAGGTAX on industrial case studies, showing that DAGGTAX not only strengthens the understanding, but also serves as the foundation of a design tool which facilitates the model-driven design of data aggregation processes.

National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-41747 (URN)10.1007/s00607-018-0679-5 (DOI)000487922400002 ()2-s2.0-85056698473 (Scopus ID)
Projects
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)
Available from: 2018-12-18 Created: 2018-12-18 Last updated: 2019-12-12Bibliographically approved
2. Tool-supported design of data aggregation processes in cloud monitoring systems
Open this publication in new window or tab >>Tool-supported design of data aggregation processes in cloud monitoring systems
Show others...
2019 (English)In: Journal of Ambient Intelligence and Humanized Computing, ISSN 1868-5137, E-ISSN 1868-5145, Vol. 10, no 7, p. 2519-2535Article in journal (Refereed) Published
Abstract [en]

Efficient monitoring of a cloud system involves multiple aggregation processes and large amounts of data with various and interdependent requirements. A thorough understanding and analysis of the characteristics of data aggregation processes can help to improve the software quality and reduce development cost. In this paper, we propose a systematic approach for designing data aggregation processes in cloud monitoring systems. Our approach applies a feature-oriented taxonomy called DAGGTAX (Data AGGregation TAXonomy) to systematically specify the features of the designed system, and SAT-based analysis to check the consistency of the specifications. Following our approach, designers first specify the data aggregation processes by selecting and composing the features from DAGGTAX. These specified features, as well as design constraints, are then formalized as propositional formulas, whose consistency is checked by the Z3 SAT solver. To support our approach, we propose a design tool called SAFARE (SAt-based Feature-oriented dAta aggREgation design), which implements DAGGTAX-based specification of data aggregation processes and design constraints, and integrates the state-of-the-art solver Z3 for automated analysis. We also propose a set of general design constraints, which are integrated by default in SAFARE. The effectiveness of our approach is demonstrated via a case study provided by industry, which aims to design a cloud monitoring system for video streaming. The case study shows that DAGGTAX and SAFARE can help designers to identify reusable features, eliminate infeasible design decisions, and derive crucial system parameters.

Place, publisher, year, edition, pages
Springer Verlag, 2019
Keywords
Cloud monitoring system design, Consistency checking, Data aggregation, Feature model, Computer software selection and evaluation, Design, Quality control, Specifications, Taxonomies, Based specification, Cloud monitoring, Efficient monitoring, Feature modeling, Large amounts of data, Propositional formulas, Monitoring
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-43881 (URN)10.1007/s12652-018-0730-6 (DOI)000469922500004 ()2-s2.0-85049591829 (Scopus ID)
Available from: 2019-06-11 Created: 2019-06-11 Last updated: 2019-09-13Bibliographically approved
3. Towards the verification of temporal data consistency in Real-Time Data Management
Open this publication in new window or tab >>Towards the verification of temporal data consistency in Real-Time Data Management
2016 (English)In: 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS, CPS Data 2016, 2016, article id Article number 7496422Conference paper, Published paper (Refereed)
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. 

Keywords
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:nbn:se:mdh:diva-32523 (URN)10.1109/CPSData.2016.7496422 (DOI)000390778200005 ()2-s2.0-84982976149 (Scopus ID)9781509011544 (ISBN)
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: 2019-09-13Bibliographically approved
4. A Formal Approach for Flexible Modeling and Analysis of Transaction Timeliness and Isolation
Open this publication in new window or tab >>A Formal Approach for Flexible Modeling and Analysis of Transaction Timeliness and Isolation
2016 (English)In: Proceedings of the 24th International Conference on Real-Time Networks and Systems, Brest, France, 2016Conference paper, Published 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
Keywords
Transaction management, concurrency control, timeliness, isolation, model checking
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-33826 (URN)10.1145/2997465.2997495 (DOI)000391255400001 ()2-s2.0-84997170469 (Scopus ID)
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: 2019-09-13Bibliographically approved
5. Specification and Automated Verification of Atomic Concurrent Real-Time Transactions
Open this publication in new window or tab >>Specification and Automated Verification of Atomic Concurrent Real-Time Transactions
2019 (English)Manuscript (preprint) (Other academic)
National Category
Software Engineering
Identifiers
urn:nbn:se:mdh:diva-45212 (URN)
Available from: 2019-09-13 Created: 2019-09-13 Last updated: 2019-09-20Bibliographically approved
6. Statistical Model Checking for Real-Time Database Management Systems: A Case Study
Open this publication in new window or tab >>Statistical Model Checking for Real-Time Database Management Systems: A Case Study
2019 (English)In: The 24th IEEE Conference on Emerging Technologies and Factory Automation ETFA2019, 2019Conference paper, Published paper (Refereed)
Abstract [en]

Many industrial control systems manage critical data using Database Management Systems (DBMS). The correctness of transactions, especially their atomicity, isolation and temporal correctness, is essential for the dependability of the entire system. Existing methods and techniques, however, either lack the ability to analyze the interplay of these properties, or do not scale well for systems with large amounts of transactions and data, and complex transaction management mechanisms. In this paper, we propose to analyze large scale real-time database systems using statistical model checking. We propose a pattern-based framework, by extending our previous work, to model the real-time DBMS as a network of stochastic timed automata, which can be analyzed by UPPAAL Statistical Model Checker. We present an industrial case study, in which we design a collision avoidance system for multiple autonomous construction vehicles, via concurrency control of a real-time DBMS. The desired properties of the designed system are analyzed using our proposed framework.

National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-45045 (URN)
Conference
The 24th IEEE Conference on Emerging Technologies and Factory Automation ETFA2019, 10 Sep 2019, Zaragoza, Spain
Projects
Adequacy-based Testing of Extra-Functional Properties of Embedded Systems (VR)
Available from: 2019-08-22 Created: 2019-08-22 Last updated: 2019-09-13Bibliographically approved

Open Access in DiVA

fulltext(2301 kB)18 downloads
File information
File name FULLTEXT01.pdfFile size 2301 kBChecksum SHA-512
c089b0a2a2f6203d7dd14220427a3b2241dbf77b576da085bbad0c02e0f872ff8ad4717b237b5b45da4b3845e3a5bc3b36d623ea52761809ede7f5eef8867f0d
Type fulltextMimetype application/pdf

Authority records BETA

Cai, Simin

Search in DiVA

By author/editor
Cai, Simin
By organisation
Embedded Systems
Software Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 18 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 108 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