ISBN 978-3-8439-1480-2

978-3-8439-1480-2, Reihe Informatik

Patrick Michel
A Formal Framework for Maintaining the Integrity of Structured Data

281 Seiten, Dissertation Technische Universität Kaiserslautern (2013), Hardcover, B5

Zusammenfassung / Abstract

Maintaining the integrity of data processed by information systems is paramount to their usefulness. We present a formal framework encompassing all concepts, languages and techniques to specify and maintain the integrity of structured data.

We define documents as a system- and paradigm-independent abstraction of data. Documents are designed to hold the information that is processed and stored by information systems and transmitted between them. Using an assertion language tailored to documents, we are able to define the common integrity constraints on real world data. The basic transactions on documents are defined using a simple update language, which is able to insert, update and delete values. Document integrity is preserved by a program, if all changes to a document are done using the basic transactions and their implementation guarantees the atomicity and consistency of their execution. For these transactions we are able to automatically derive the weakest preconditions which provide these guarantees, by applying syntactic transformations to the integrity constraints. Furthermore, we are able to normalize the preconditions such that the necessary incremental checks on the transaction parameters and the document can be identified.

We have taken a rigorous approach to showing the soundness of our technique and the critical parts of its implementations, by deeply embedding our theory into the framework of higher-order logic and mechanizing all proofs in the theorem prover Isabelle/HOL. We have implemented an example system, which is in productive use, showing that the assertion and update languages are practically relevant. The syntax transformers of the theory are used in a prototypical tool chain, which allows the creation of Java libraries from document schemata.