Master of Science in Software Engineering, Cleveland State University, 2014, Washkewicz College of Engineering

FreeRTOS is a popular real-time and embedded operating system. Real-time software requires code reviews, software tests, and other various quality assurance activities to ensure minimal defects. This free and open-source operating system has claims of robustness and quality [26]. Real-time and embedded software is found commonly in systems directly impacting human life and require a low defect rate. In such critical software, traditional quality assurance may not suffice in minimizing software defects. When traditional software quality assurance is not enough for defect removal, software engineering formal methods may help minimize defects. A formal method such as program verification is useful for proving correctness in real-time soft- ware. Microsoft Research created Dafny for proving program correctness. It contains a programming language with specification constructs. A program verification tool such as Dafny allows for proving correctness of FreeRTOS's modules. We propose using Dafny to verify the correctness of FreeRTOS' scheduler and supporting API.

Committee: Nigamanth Sridhar PhD (Committee Chair); Yongjian Fu PhD (Committee Member); Chansu Yu PhD (Committee Member) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2024, Computer Science and Engineering

Unmanned Aerial Systems (UAS) are increasingly important. Farmers monitor crops and apply pesticides with UAS. First responders use UAS in applications ranging from fire fighting to search and rescue operations. There is potential for rapid shopping delivery by UAS. In all these applications, UAS work closely alongside humans. Onboard firmware controls the behavior of UAS. This dissertation studies ways to improve the quality of firmware. We start by presenting the first large-scale analysis of software defects ("bugs") reported in open-source UAS firmware. We examine nearly 300 reported bugs in the two most popular open-source systems (ArduPilot and PX4) and categorize the defects. Motivated by our findings, we propose three technologies to automate the detection and repair of UAS bugs. First, Avis seeks to automatically diagnose sensor bugs caused by misusing onboard sensors. Second, SA4U identifies unit type errors caused by incorrectly mixing values with different physical unit types (e.g., meters and minutes) in a computation. Finally, Scalpel automatically repairs bugs found by SA4U. Deep learning is increasingly used to provide advanced autonomous behavior for UAS. To support higher quality deep learning systems we propose checkd. Checkd automates checkpoint/restore policy configurations. Underlying checkd's contribution is the thesis that better tuned models yield better behavior. Checkd helps practitioners fine-tune models by reducing the overall cost to train.

Committee: Feng Qin (Advisor); Michael Bond (Committee Member); Christopher Stewart (Committee Member) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2011, Computer Science and Engineering

In order to have more confidence in software-based systems, we would like to be able to show automatically that a particular software component meets its specification; the component does what it is supposed to do. Testing can increase confidence in software; however, testing alone cannot show that software meets its specification, only that no errors have been found yet. We are building stronger tools for increasing our confidence in software in response to the verifying compiler grand challenge. The vision is that all software will include specifications for all of the operations of a component (including pre- and post-conditions) along with code annotations in a purported implementation (including loop invariants, and progress metrics for the termination of both loops and recursive operations). These annotations allow us to generate verification conditions (VCs) that represent the correctness of the code mathematically. The code meets its specification and is correct if the VCs are proved. We focus on the problem of automating VC proofs and examining potential obstacles for automated proofs. More specifically, this dissertation defends the following three-part thesis: 1. Modest changes in programming languages may effectively support and facilitate automated verification without introducing an undue annotation burden on programmers. 2. An interactive proof assistant can be an effective back-end prover for automated software verification. 3. Translations between similar formal systems present significant challenges in fully automating software verification.

Committee: Bruce W. Weide PhD (Advisor); Paul A. G. Sivilotti PhD (Committee Member); Michael D. Bond PhD (Other) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2011, Computer Science and Engineering

For a variety of reasons, software must evolve to cope with change. Unfortunately, evolution and maintenance is an expensive, time-consuming, and error-prone task, especially when the system in question is large and complex. Typically, a change to a single program element requires changes to related, and often seemingly unrelated, elements scattered throughout the source code. To address this problem, approaches have emerged to mechanically assist developers with a wide range of software evolution and maintenance tasks. This assistance is typically provided in the form of extensions (plug-ins) to integrated development environments (IDEs) that afford (semi-) automated aid in carrying out these tasks, thus easing the burden associated with evolution and maintenance. Although existing approaches are useful in alleviating some of the burden associated with software evolution and maintenance, there are a number of situations where developers are still required to complete evolution and maintenance tasks manually. Automated approaches to assist developers with such cumbersome and error-prone tasks would be extremely useful in evolving and maintaining large, complex systems. In this thesis, I develop several new techniques that can be of great value to software developers in evolving code to accommodate change. The first is an automated refactoring that upgrades legacy Java code to use proper language enumeration (enum) types, a feature of the modern Java language. I have developed an approach that preserves semantics and that allows us to migrate legacy applications by automatically replacing a predominantly used pattern with suitable use of enums. The second technique is an automated approach to assist developers in maintaining pointcuts in evolving Aspect-Oriented (AO) programs. AO languages enable developers to better encapsulate crosscutting concern (CCC) implementations by allowing them to create an expression (a pointcut) which specifies well-defined points ( (open full item for complete abstract)

Committee: Neelam Soundarajan PhD (Advisor); Atanas Rountev PhD (Committee Member); Paul A. G. Sivilotti PhD (Committee Member); Paul Evans PhD (Committee Member) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2010, Computer Science and Engineering

Numerous pieces of the software verification puzzle need to fit together in order to achieve that vision. First, there must be a programming language that gives some hope of specifying and implementing verifiable code ("assertive code"). Second, there needs to be a correct procedure for generating verification conditions (VCs) from this assertive code. Third, there must be one or more automated theorem provers to process the VCs and determine their validity or invalidity. Finally, it is essential that there is an interface for programmers to write their code and verify or debug it without forcing them to understand how particular automated theorem provers work. This dissertation covers the latter two of these topics using the Resolve language and verification framework. A common failing of most automated verification techniques is the inability to be truly automatic in all circumstances. Experience with proof assistants shows that they need to be "nudged" in the correct direction by an intervening human, in all but the simplest cases. Otherwise, the option is to use tools not geared to handle the rich mathematics used in the Resolve programming language. By using specialized decision procedures that take into account the known structure of the generated VCs, we strive to accomplish one of two possibilities for each VC: first, we hope to prove it outright; otherwise, we hope to simplify the VC to such an extent that another prover is able to handle it. We detail work on SplitDecision, a tool that simplifies VCs for Resolve. We further explain work that has helped to ensure SplitDecision is among the fastest and least memory intensive automated provers available, by introducing "lazy copying" to Resolve/C++ (in which SplitDecision is written), with specific work to maintain the value semantics integral to Resolve's design. Sometimes (perhaps this is even the modal case) at least one VC is not proved because it is not valid. It is clear that the ways we present errors (open full item for complete abstract)

Committee: Bruce Weide PhD (Advisor); Atanas Rountev PhD (Committee Member); Paolo Sivilotti PhD (Committee Member); Melvin Pascall PhD (Committee Member) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2021, Computer Science and Engineering

Modular verification of parallel and concurrent software built from reusable data abstractions is a challenging problem. Reasoning about sequential software can be modularized using the specifications of data abstractions, but the need to consider implementation details complicates reasoning about parallel execution. Addressing this challenge requires advancing the state of the art in several ways, beginning with a theoretical foundation. The A/P Calculus for describing the effects of program actions is developed in this dissertation to enable sound modular reasoning about parallel programs with non-interfering parallel sections of operation calls on abstract data types. Building on the calculus and a programming language with clean semantics, a methodology for designing decomposable data abstractions is presented to produce fork-join parallel programs that are manifestly data race free and readily amenable to modular reasoning. A new specification construct, the non-interference contract, is proposed to enhance the specification of data abstractions to hide implementation details and yet facilitate modular reasoning about parallel programs that share objects among processes. As a key first step to transition these results to practice, this dissertation describes Clean++, a discipline for writing software in C++ that leverages move semantics to make ownership transfer the primary data movement operation (as opposed to either deep or shallow copying) and produce programs that are amenable to formal verification with only minimal scaffolding related to pointer manipulation.

Committee: Paolo A.G. Sivilotti (Advisor); Murali Sitaraman (Committee Member); Neelam Soundarajan (Committee Member); Michael Bond (Committee Member) Subjects: Computer Science

Master of Science (MS), Ohio University, 2021, Electrical Engineering & Computer Science (Engineering and Technology)

Reinforcement learning is a growing field of research, but little work is being done to verify the correctness of reinforcement learning algorithms. Researchers are exploring the use of reinforcement learning in safety critical systems such as self-driving cars and autonomous aircraft, so mathematical proofs of correctness of the underlying reinforcement learning algorithms would greatly improve our confidence in the systems that utilize reinforcement learning. This project verifies convergence and optimality of two fundamental reinforcement learning algorithms: value iteration and policy iteration. These algorithms converge and are optimal if they eventually produce an optimal policy. It also is designed to be extensible to future research into verified reinforcement learning.

Committee: Gordon Stewart (Advisor); Bunescu Razvan (Committee Member); Juedes David (Committee Member); Elster Charlotte (Committee Member) Subjects: Computer Science

Master of Science (MS), Ohio University, 2020, Electrical Engineering & Computer Science (Engineering and Technology)

Machine learning algorithms are integrated into many aspects of daily life. However, research into the correctness and security of these important algorithms has lagged behind experimental results and improvements. My research seeks to add to our theretical understanding of the Perceptron family of algorithms, which includes the Kernel Perceptron, Budget Kernel Perceptron, and Description Kernel Perceptron algorithms. In this thesis, I will describe three variants of the Kernel Perceptron algorithm and provide both proof and performance results for verified implementations of these algorithms written in the Coq Proof Assistant. This research employs generalization error, which bounds how poorly a model may perform on unseen testing data, as a guarantee of performance with proofs verified in Coq. These implementations are also extracted to the functional language Haskell to evaluate their generalization error and performance results on real and synthetic data sets.

Committee: Gordon Stewart (Advisor); David Juedes (Committee Member); Razvan Bunescu (Committee Member) Subjects: Artificial Intelligence; Computer Science

Master of Science (MS), Ohio University, 2016, Computer Science (Engineering and Technology)

Errors in programs and mathematical results are a common cause for wasted time and resources. While peer-review and software-engineering techniques are helpful in mitigating the occurrence of these errors, the human element at the center of these techniques is fallible, and for very large or complex results the application of these techniques is often infeasible. Towards this end, researchers have developed a number of tools, proof assistants, which aid the user in constructing machine-checkable formal proofs. Tools and theories verified using these tools carry a much stronger assurance of correctness than many alternatives. Currently, a number of fundamental theorems and programs have been proven correct within these proof assistants, as well as a number of proofs which were previously deemed too large for review. However, despite these successes, and the ubiquity of graph algorithms in computer science, little work has been done towards generating verified implementations of graph algorithms. This thesis describes my attempt to address this weakness through the construction of a verified implementation of Tsukiyama et al.'s algorithm for enumerating all maximal independent sets of a graph. The enumeration of all maximal independent sets has a number of immediate applications in domains such as computer vision, computational chemistry and information systems, as well as being an important subroutine in efficient algorithms for exact graph coloring. Such a verified algorithm could lay the foundation for a library of verified graph algorithms suitable for use in critical systems.

Committee: David Juedes PhD. (Advisor); Gordon Stewart PhD. (Committee Member); Chang Liu PhD. (Committee Member); Archil Gulisashvili PhD. (Committee Member) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2016, Computer Science and Engineering

Current tools used to verify software in languages with reference semantics, such as Java, are hampered by the possibility of aliases. Existing approaches to addressing this long-standing verification problem try not to sacrifice modularity because modular reasoning is what makes verification tractable. To achieve this, these approaches treat the value of a reference variable as a memory address in the heap. A serious problem with this decision is that it severely limits the usefulness of generic collections because they must be specified as collections of references, and components of this kind are fundamentally flawed in design and implementation. The limitations become clear when attempting to verify clients of generic collections. The first step in rectifying the situation is to redefine the "value" of a reference variable in terms of the abstract value of the object it references. A careful analysis of what the "value" of a reference variable might mean leads inevitably to this conclusion, which is consistent with the denotation of a variable in languages with value semantics, such as RESOLVE. Verification in languages with value semantics is straightforward compared to verification in languages with reference semantics precisely because of the lack of concern with heap properties. However, there is still a nagging problem: aliasing can occur in legal programs in languages with reference semantics, such as Java, and it must be handled when it does occur. The crux of the issue is not in-your-face assignment statements that copy references but rather aliasing arising within (hidden) method bodies. The reason is that the effects of calls to these methods in client code must be summarized in their specifications in order to preserve modularity. So, the second step is the introduction of a discipline restricting what a client can do with a reference that is aliased within a method. The discipline advertises the creation of such aliases in method speci (open full item for complete abstract)

Committee: Bruce W. Weide (Advisor); Neelam Soundarajan (Committee Member); Paul A. G. Sivilotti (Committee Member) Subjects: Computer Science

Master of Science, The Ohio State University, 2013, Mechanical Engineering

The global automotive industry continually strives to develop advanced automotive control systems that can reduce fuel consumption and emissions towards a greener future, while improving efficiencies and enhancing safety and comfort.This effort is collaborative, with not just OEMs and their suppliers working amidst stiff competition and strict regulations, but various research organizations, both independent as well as academic collaborating with these OEMs. As a result of this collaborative effort, there is a huge potential for synergy, but also the possibility of huge disconnects in the process itself. Model-Based System Development methodologies that use simulation models representing the controlled and controlling systems have a very important role to play in today's scenario when developing control systems. For a research organization with strong academic background such as the Center for Automotive Research at The Ohio State University, a comprehensive process for automotive model-based control that encapsulates various practice and standards already in place in the industry can help develop better solutions when collaborating with industry. While systematic and detailed approaches exist already, there are sufficient variations amongst internal approaches and methodologies which calls for a more unified approach that is industry-inspired. This thesis presents a comprehensive process that helps a developer gain an overall perspective to the bigger problem. The proposed methodology starts right at the fundamental opportunity identification phase, and is driven in the early stages by product development methodologies. Systematic approaches towards identifying opportunities, generating concepts and selecting concepts, with a case-study based on the usage of model-based simulations tools to select concepts are presented. With constantly changing requirements in the automotive industry, the need for traceability to the initial requirements has b (open full item for complete abstract)

Committee: Shawn Midlam-Mohler PhD (Advisor); Giorgio Rizzoni PhD (Committee Member); Marcello Canova PhD (Committee Member); Fabio Chiara PhD (Committee Member) Subjects: Automotive Engineering

Doctor of Philosophy, The Ohio State University, 2012, Computer Science and Engineering

Abstraction is our most powerful tool for understanding the universe scientifically. In computer science, the term “abstraction” is overloaded, and its referents have not been enunciated with sufficient clarity. A deep understanding of what abstraction is and the different ways it can be employed would do much to strengthen both the research and the practice of software engineering. Specifically, this work focuses on abstraction into pure mathematics as it pertains to the intellectual complexity of computer programming. A Grand Challenge for software engineering research is to develop a verifying compiler, which takes as input a computer program and a rigorous specification of its intended behavior, and which only generates an executable if the code is proven correct via automated reasoning. The hypothetical verifying compiler would radically change the face of technology by guaranteeing that code always behaves as it should. We investigate the ways in which good abstractions, maximally exploited, can make this dream a reality. This document presents, at varying levels of technical detail, evidence for the utility of abstractions in software. We show how standard approaches to programming, even in the realm of “formal methods,” lack full abstraction. We argue that data abstraction should be achieved via purely mathematical modeling, and that this approach enables modular, scalable verification of complete system behavior. We also warn that a programming language's formal semantics can dramatically impact the feasibility of a verifying compiler for that language. One of our main results is that the class of “functional” programming languages cannot be soundly verified by the pervasive existing methods due to an insidious and subtle issue related to data abstraction and relational specifications. We build on this unsoundness proof by sketching a new solution, and fragments of a new functional programming language that incorporates it.

Committee: Dr. Bruce W. Weide PhD (Advisor); Dr. Atanas Rountev PhD (Committee Member); Dr. Paul Sivilotti PhD (Committee Member) Subjects: Computer Engineering; Computer Science

Master of Science (MS), Ohio University, 2007, Computer Science (Engineering)

This thesis constitutes an effort of verifying and validating a safety system designed for a specific research facility. An initial comprehensive review of the system design is presented, detailing all the relevant aspects of the system and investigating the way its design development interrelates to the formal "safety analysis" procedures proposed in the literature. The verification process includes the development of a complete formal specification for the system and the investigation of how well the original design follows its formal requirements. The validation process details the system's hardware and software implementations, discusses the testing approach, and evaluates the final outcomes. In summary, this work can be considered as an effort to prove that the operation of the laboratory in question, within the designed safety system's scope, is safe.

Committee: Frank Drews (Advisor) Subjects: