Theses and Dissertations from UMD
Permanent URI for this communityhttp://hdl.handle.net/1903/2
New submissions to the thesis/dissertation collections are added automatically as they are received from the Graduate School. Currently, the Graduate School deposits all theses and dissertations from a given semester after the official graduation date. This means that there may be up to a 4 month delay in the appearance of a give thesis/dissertation in DRUM
More information is available at Theses and Dissertations at University of Maryland Libraries.
Browse
2 results
Search Results
Item Learning Temporal Properties from Data Streams(2020) Huang, Samuel; Cleaveland, Rance; Computer Science; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)Verifying that systems behave as expected is a cornerstone of computing. In formal verification approaches, engineers capture their intentions, or specifications, mathematically, often using logic. The verification task is then to confirm that the system satisfies its specifications. In a formal setting this endeavor typically involves the construction of mathematical proofs, which are either constructed automatically, as in the case of so-called model-checking techniques, or by humans with machine assistance, as in the case of theorem-proving-based methodologies. In practice, formal verification faces a number of obstacles. One involves the construction of formal specifications in the first place. Another is the lack of availability of analyzable system artifacts (source code, executables) about which proofs can be constructed. In this dissertation we propose techniques for inferring formal specifications, in the form of Linear Temporal Logic formulas, from system executions, and models when these are available, as a means of addressing these concerns. We first illustrate how guided generation of test cases (i.e. guided exploration of the system's input/output space) can be leveraged to develop and then refine the hypothesis set of invariants that a system satisfies. This approach was successful in revealing a system property required in code specification of an automotive application provided to us but missing in the implementation. An unexpected (undocumented) specification was also discovered through our analysis. The approach has since been applied by other researchers to several other automotive applications. Second, we develop techniques to mine properties from models of systems and/or their executions. In some cases compact, finite state representations of a system is available. In this scenario we employ a novel automaton-based approach to mine properties matching a user-specified template. In other cases such white-box knowledge is not available and we must work over executions of the system rather than the system itself. In this scenario we apply a novel variant of Linear Temporal Logic (LTL) using finite-sequence semantics to again mine properties based on a specified template. Lastly, we consider situations where standard formal properties are insufficient due to uncertainty or being overly simplified. Oftentimes properties that are not satisfied 100\% of the time can be very interesting during a system inspection or system redesign. For example, natural noise manifesting in data streams from system executions such as missing evidence and changing system behavior could lead to significant properties being overlooked if a strict ``exactitude'' were enforced. We explore the notion of ``incomplete'' properties which we term \emph{partial invariants} by formulating a new ``Noisy Linear Temporal Logic'' which is an extension of standard LTL. We consider several representations of such noise and show decidability of the language emptiness problem for some of the variants.Item Towards a Unified Theory of Timed Automata(2014) Fontana, Peter Christopher; Cleaveland, Rance; Computer Science; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)Timed automata are finite-state machines augmented with special clock variables that reflect the advancement of time. Able to both capture real-time behavior and be verified algorithmically (model-checked), timed automata are used to model real-time systems. These observations have led to the development of several timed-automata verification tools that have been successfully applied to the analysis of a number of different systems; however, the practical utility of timed automata is undermined by the theories underlying different tools differing in subtle but important ways. Since algorithmic results that hold for the variant used by one tool may not apply to another variant, this complicates the application of different tools to different models. The thesis of this dissertation is this: the theory of timed automata can be unified, and a practical unified approach to timed-automata model checking can be built around the paradigm of proof search. First, this dissertation establishes the mutual expressivity of timed automata variants, thereby providing precise characterizations of when theoretical results of one variant apply to other variants. Second, it proves powerful expressive properties about different logics for timed behavior, and as a result, enlarges the set of verifiable properties. Third, it discusses an implementation of a verification tool for an expressive fixpoint-based logic, demonstrating an application of this newly developed theory. The tool is based on a proof-search paradigm; verifying timed automata involves constructing proofs using proof rules that enable verification problems to be translated into subproblems that must be solved. The tool's performance is optimized by using derived proof rules, thereby providing a theoretically sound basis for faster model checking. Last, this dissertation utilizes the proofs generated during verification to gain additional information about the vacuous satisfaction of certain formulae: whether the automaton satisfied a formula by never satisfying certain premises of that specification. This extra information is often obtained without significantly decreasing the verifier's performance.