Runtime verification, as a field, provides tools to describe how programs should behave during execution, allowing programmers to inspect and enforce properties about their code at runtime. This field has resulted in a wide variety of approaches to inspecting and ensuring correct behavior, from instrumenting individual values in order to verify global program behavior to writing ubiquitous predicates that are checked over the course of execution. Although each verification approach has its own merits, each has also historically required ground-up development of an entire framework to support such verification.
In this work, we start with software contracts as a basic unit of runtime verification, exploring the myriad of approaches to enforcing them—ranging from the straightforward pre-condition and post-condition verification of Eiffel to lazy, optional, and parallel enforcement strategies—and present a unified approach to understanding them, while also opening the door to as-yet-undiscovered strategies. By observing that contracts are fundamentally about communication between a program and a monitor, we reframe contract checking as communication between concurrent processes. This brings out the underlying relations between widely-studied verification strategies, including strict and lazy enforcement as well as concurrent approaches, including new contracts and strategies. We introduce a concurrent core calculus (with proofs of type safety), show how we may encode each of these contract verification strategies in it, and demonstrate a proof (via simulation) of correctness for one such encoding.
After demonstrating this unified framework for contract verification strategies, we extend our verification framework with meta-strategy operators—strategy-level operations that take one or more strategies (plus additional arguments) as input and produce new verification behaviors—and use these extended behavioral constructs to optimize contract enforcement, reason about global program behavior, and even perform runtime instrumentation, ultimately developing multiple runtime verification behaviors using our communication-based view of interaction.
Finally, we introduce an extensible, Clojure-based implementation of our framework, demonstrating how our approach fits into a modern programming language by recreating our contract verification and general runtime verification examples.
|Commitee:||Moss, Lawrence S., Siek, Jeremy, Tobin-Hochstadt, Sam|
|School Location:||United States -- Indiana|
|Source:||DAI-B 80/07(E), Dissertation Abstracts International|
|Keywords:||Concurrency, Runtime, Semantics, Verification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be