<p> 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. </p><p> 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. </p><p> 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. </p><p> 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.</p><p>
| Identifer | oai:union.ndltd.org:PROQUEST/oai:pqdtoai.proquest.com:13806256 |
| Date | 23 March 2019 |
| Creators | Swords, Cameron |
| Publisher | Indiana University |
| Source Sets | ProQuest.com |
| Language | English |
| Detected Language | English |
| Type | thesis |
Page generated in 0.0104 seconds