A Methodology for Automated Verification of Rosetta Specification Transformations
Issue Date
2011-04-11Author
Lohoefener, Jennifer Lee
Publisher
University of Kansas
Format
153 pages
Type
Dissertation
Degree Level
Ph.D.
Discipline
Electrical Engineering & Computer Science
Rights
This item is protected by copyright and unless otherwise specified the copyright of this thesis/dissertation is held by the author.
Metadata
Show full item recordAbstract
The Rosetta system-level design language is a specification language created to support design and analysis of heterogeneous models at varying levels of abstraction. These abstraction levels are represented in Rosetta as domains, specifying a particular semantic vocabulary and modeling style. The following dissertation proposes a framework, semantics and methodology for automated verification of safety preservation over specification transformations between domains. Utilizing the ideas of lattice theory, abstract interpretation and category theory we define the semantics of a Rosetta domain as well as safety of specification transformations between domains using Galois connections and functors. With the help of Isabelle, a higher order logic theorem prover, we verify the existence of Galois connections between Rosetta domains as well as safety of transforming specifications between these domains. The following work overviews the semantic infrastructure required to construct the Rosetta domain lattice and provides a methodology for verification of transformations within the lattice.
Collections
- Dissertations [4701]
- Engineering Dissertations and Theses [1055]
Items in KU ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
We want to hear from you! Please share your stories about how Open Access to this item benefits YOU.