Graduate Thesis Or Dissertation
 

Formal Verification of the Variational Database Management System

Public Deposited

Downloadable Content

Download PDF
https://ir.library.oregonstate.edu/concern/graduate_thesis_or_dissertations/qf85nj87k

Descriptions

Attribute NameValues
Creator
Abstract
  • Variation in data is abundant and ubiquitous in real-world applications. Managing variation in databases is, however, difficult and has been extensively studied by the database community. Schema evolution, data integration, and database versioning are examples of well-studied forms of database variation with effective context-specific solutions. However, variation appears in different forms and contexts in databases, and existing approaches cannot be generalized to handle arbitrary forms of variation irrespective of the context. Moreover, in practice, different forms of variation intersect in a particular context. Variational databases (VDB) provide a fundamental solution to variation management by explicitly encoding variation into relational databases that allows addressing different kinds of variation simultaneously. To support expressing variation in information need, traditional relational algebra (RA) is extended to variational relational algebra (VRA). VRA comes with a static type system that checks the validity of variational queries written in VRA. This thesis extends the formalization and formally verifies properties of the variational database management system (VDBMS). Variational sets and set operations definitions are formally verified and VDBs are formally encoded using them. Then, the correctness of the VRA type system with respect to the RA type system is formally specified and verified. VDBMS also allows writing variational queries with-out repeating variations that are already encoded in the VDB and sub-queries. These implicitly annotated v-queries get explicitly annotated by the system. Therefore, this thesis further formally verifies the process of explicitly annotating variational queries.
License
Resource Type
Date Issued
Degree Level
Degree Name
Degree Field
Degree Grantor
Commencement Year
Advisor
Committee Member
Academic Affiliation
Rights Statement
Publisher
Peer Reviewed
Language
File Format

Relationships

Parents:

This work has no parents.

In Collection:

Items

Thumbnail Title Date Uploaded Visibility Actions
file details KhanFariba2021.pdf 2021-04-21 Public Download