Doctor of Philosophy (Ph.D.), Bowling Green State University, 2014, Statistics

The predominant model checking method used in Bayesian item response theory (IRT) models has been the posterior predictive (PP) method. In recent years, two new Bayesian model checking methods have been proposed that may be used as alternatives to the PP method. We refer to these as the prior-predictive posterior simulation (PPPS) method of Dey et al. (1998), and the pivotal discrepancy measure (PDM) method of Johnson (2007). These methods have shown to be effective in other Bayesian models, but have never been implemented with Bayesian IRT models. It is of practical interest to see if either of these two new methods will perform better than the PP method in assessing aspects of fit in an IRT model setting. In this dissertation, we compared the effectiveness of the PPPS and PDM model checking methods with the PP method in evaluating person fit in two-parameter normal ogive (2PN) IRT models, and overall model goodness-of-fit in 2PN testlet models. Two simulation studies were performed. The first study explored the performance of each method (PP, PPPS, and PDM) in assessing person fit, or the goodness-of-fit of an individual's set of test answers with the assumed Bayesian 2PN IRT model. Several classical person fit measures were employed under each method. We also introduced using the sum of squared Bayesian latent residuals as a person fit measure. Four different types of person miss-fit were taken from the literature, and response data sets were simulated with certain examinee's responses following these violations. We found that for most of the measures, the PPPS and PDM methods outperformed the PP method in detecting the examinee's response patterns simulated to be aberrant under the model. In particular, the sum of squared Bayesian latent residuals showed to be a very effective measure under the PPPS method. The second simulation study compares the performance of the PP method and the PPPS method in assessing the overall goodness-of-fit of (open full item for complete abstract)

Committee: James Albert (Advisor); Lynne Hewitt (Committee Member); Hanfeng Chen (Committee Member); Maria Rizzo (Committee Member) Subjects: Statistics

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

PhD, University of Cincinnati, 2024, Engineering and Applied Science: Computer Science and Engineering

Hardware security threats can be introduced at various stages of the System-on-Chip design life cycle. These threats manifest in the design as unwarranted design modifications and malicious backdoor insertions, which result in critical information leakage or denial of service. Thus, it is essential to verify these complex SoC designs at various stages of their life cycles. Verifying such complex designs is a critical and laborious task and consumes 70% of the design effort. Formal verification techniques offer significant performance compared to traditional functional verification strategies by using mathematical principles to identify critical corner cases that functional methods often miss. When a formal property fails for a given design, a counterexample is produced, providing evidence of failure. This counterexample includes a sequence of inputs that can be converted into test vectors for use in post-silicon verification. Despite offering an automated framework for bug detection, formal methods do not automatically pinpoint the exact location of these bugs or security vulnerabilities within the design. Formal verification engineers still need to manually analyze the counterexample and identify the precise location of the vulnerability and the reason behind the assertion failure. Some SATbased techniques attempt to localize bugs at the gate level of the System-on-Chip design by introducing additional test point hardware, such as multiplexers. However, these techniques are inefficient for complex SoC designs as they need to be represented in their conjunctive normal form leading to significant compatibility issues. Thus, we levitate toward model checkers which offer a more simplistic approach to property verification. This research intends to develop tools that leverage model checkers to localize a variety of security violations that fail security assertions and develop a wide range of test vectors to det (open full item for complete abstract)

Committee: Ranganadha Vemuri Ph.D. (Committee Chair); Wen-Ben Jone Ph.D. (Committee Member); Suyuan Chen Ph.D. (Committee Member); Boyang Wang Ph.D. (Committee Member); John Emmert Ph.D. (Committee Member) Subjects: Engineering

PhD, University of Cincinnati, 2021, Engineering and Applied Science: Computer Science and Engineering

Logic encryption, a prominent solution to the hardware IP security problem, protects a circuit by adding 'encryption' logic to lock the design functionality using a set of newly introduced key inputs. Logic encryption for combinational circuits focuses on adding combinational gates as encryption logic. When encrypting sequential circuits, most techniques advocate the modification of the FSM to either prevent entering normal operation or force the design into corrupted state(s) on the application of a wrong key. Another avenue taken by sequential logic encryption is to lock the scan-chains by inserting key gates on the scan connections between the flip-flops in the circuit to reduce the ability to set and observe the internal state of the circuit. Boolean satisfiability based attack methods are successful in decrypting combinational logic encrypted circuits. Subsequently proposed SAT-resilient techniques are susceptible to other type of attacks like removal, bypass or functional analysis attacks. Although SAT methods can be used to attack sequential circuit using scan chains, this approach is rendered ineffective if the scan chains are absent or are locked using key gates, as described above. Due to these limitations, sequential logic encryption techniques claim SAT-resiliency. One of the goals of this dissertation is to test the validity of this claim by developing SAT-based attack methods that can attack logic encrypted sequential circuits without scan access. Circuit unrolling is a promising technique that is used to develop such an attack method. The decryption efficiency of this attack is evaluated against modern sequential logic encryption techniques. Furthermore, more robust and highly effective encryption techniques to counter the sequential SAT attack method are proposed in this work by analyzing the attributes of the attack that contribute towards its success against other sequential logic encryption schemes. Emphasis is placed on extracting information re (open full item for complete abstract)

Committee: Ranganadha Vemuri Ph.D. (Committee Chair); Mike Borowczak Ph.D. (Committee Member); John Emmert Ph.D. (Committee Member); Wen-Ben Jone Ph.D. (Committee Member); Carla Purdy Ph.D. (Committee Member) Subjects: Computer Engineering

MS, University of Cincinnati, 2018, Engineering and Applied Science: Computer Engineering

Modern digital era empowers the resurgence of the Internet of Things (IoT) concept proposed back in the 1980s. IoT applications involve a network of embedded systems that can share information amongst them. The present-day Integrated Circuits (ICs) get smaller and smaller driven by Moore's law and allows designers to embed enhanced functionalities on these tiny devices. Due to the outsourcing of the design at multiple stages in the IC design flow, state of the art ICs are vulnerable to the intervention by third-party vendors. Hence, there are concerns over security and reliability of the hardware. One particularly stealthy yet intrusive way of undermining the security of an IC is through the insertion of Hardware Trojans in the design. A hardware Trojan is a malicious circuit inserted into the genuine circuit without the designer's knowledge. Predominantly adopted Design for Testability (DFT) approach involves the inclusion of scan chain in sequential logic designs to improve testability but adds area and pin overhead on the overall chip. Due to severe area and cost constraints, sequential circuits often used in IoT devices do not consist of scan chains. Malicious Trojan circuits, which themselves may be state machines, inserted into such systems are hard to detect. We present an effective methodology to detect sequential Trojan circuits inserted into sequential hardware designs without scan chains typically used in IOT applications. The methodology consists of three steps: I. Sequential testability metrics are used to identify nets susceptible to Trojan insertion (suspect nets). II. Model checking technique is utilized to determine the length of the activation sequences of suspect nets obtained from the previous step. Nets with longer activation sequences are classified as Trojan nets. III. Finally, a signal tracing and classification algorithm is proposed to trace back from payload circuit of Trojan to progressively separate the Trojan net (open full item for complete abstract)

Committee: Ranganadha Vemuri Ph.D. (Committee Chair); Wen-Ben Jone Ph.D. (Committee Member); Carla Purdy Ph.D. (Committee Member) Subjects: Computer Engineering

MS, University of Cincinnati, 2017, Engineering and Applied Science: Electrical Engineering

In recent years, the semiconductor industry has enthusiastically adopted the fabless model of chip fabrication i.e. fabricating designs through third party vendors. With modernization and automation, the role of IC's in the control and operation of systems has become a critical component. It is therefore important that the security of the underlying hardware not be compromised. Implanting Hardware Trojans is a stealthy and intrusive way of undermining the security of hardware. With designs being fabricated by 3rd parties, it is difficult to guarantee that the fabricated product is 100% secure. In recent years, many methods have been presented to detect Hardware Trojans. These include using timing, power, capacitance as parameters to detect the presence of a Trojan. While these methods can detect Trojans whose size is comparable to the genuine circuit size, they do not perform as expected for smaller Trojans as the impact of a small Trojan on these parameters is negligible. On the other hand, functional methods fare better in detecting smaller Trojans. In this work, we use a controllability and observability based metric followed by symbolic model checking to discover the Trojan nodes in the design. We show several experimental results to demonstrate the validity of the approach.

Committee: Ranganadha Vemuri Ph.D. (Committee Chair); Wen-Ben Jone Ph.D. (Committee Member); Carla Purdy Ph.D. (Committee Member) Subjects: Engineering

MS, University of Cincinnati, 2016, Engineering and Applied Science: Aerospace Engineering

In recent years, there have been huge advances in controllers used in autonomous systems. One particular area of research is Fuzzy Logic Controllers (FLCs) that are trained by both expert knowledge-based optimization algorithms such as Genetic Algorithms (GAs). GAs represent a particularly powerful way to optimize a FLC as they often perform better than other search algorithms when the state space is rather complex. A downside to these systems however is that their functionality is difficult to verify due to highly non-linear behavior. Typical verification involves Monte Carlo type simulations that require time to perform and may miss critical test points. Therefore, there is a need for more formal ways of verifying the correctness of FLCs based on specifications set forth for their operation over the entire state space. In this work, a method of converting a 2-input 1-output FLC with specific constraints into a Piecewise Affine Hybrid System (PWAHS) is extended to a 3-input 1-output case for implementation of a cascaded FLC system. Verification of safety properties of the converted PWAHS using Formal Methods tools is then conducted. FLCs were then created for a case study involving both one and two degree-of-freedom inverted pendulum systems and trained with Genetic Algorithms. Specifications about their functionality were derived from expert knowledge of the system and simulation results. The specifications were translated into temporal logic specifications that could then be checked by Symbolic Model Checkers (SMCs) utilizing Satisfiability Modulo Theories (SMT) solvers. It is shown that the FLCs created are shown to meet the requirements set forth, and in cases where they do not, generated counterexamples give a point in the state space where they are violated. FLCs that violated the properties were then re-trained and checked again using specifications derived from simulation results. The final FLC was shown to meet all safety specifications under all condition (open full item for complete abstract)

Committee: Kelly Cohen Ph.D. (Committee Chair); Matthew A. Clark M.S. (Committee Member); Nicholas D. Ernest Ph.D. (Committee Member); Manish Kumar Ph.D. (Committee Member) Subjects: Aerospace Materials

Doctor of Philosophy, The Ohio State University, 2004, Computer and Information Science

We define a game of pursuers seeking evaders on a grid, originally motivated by, but not limited to, the problem of unmanned aerial vehicles searching for moving targets. The pursuers have a speed advantage over the evaders but are incapable of determining an evader's location unless a pursuer occupies the same location as that evader. The evaders, on the other hand, operate with unlimited luck and cunning: if it is possible for them to avoid the pursuers, they will. By treating the players as nondeterministic finite automata, we can model the game and use it as the input for a model checker. While model checkers normally are used to verify program correctness, we use the model checker to generate a pursuer-winning search strategy. We demonstrate this technique for the full model and then develop heuristics to reduce the model so we can address larger problem sizes. We further prove an upper bound on the minimum pursuer-winning speed; moreover, we show the bound is tight for a particular class of search strategies.

Committee: Paolo Sivilotti (Advisor) Subjects: Computer Science

Doctor of Philosophy, Case Western Reserve University, 2006, Computer Engineering

Bounded Model Checking (BMC) is a formal method of verifying Very Large Scale Integrated (VLSI) circuits. It shows violation of a given circuit property by finding a counter-example to the property along bounded state paths of the circuit. The BMC problem is inherently NP-complete and is traditionally formulated to a boolean SATisfiability (SAT) problem, which is subsequently solved by a SAT solver. Automatic Test Pattern Generation (ATPG), as an alternative to SAT, has already been shown an effective solution to NP-complete problems in many computer-aided design areas. In the field of BMC, ATPG has already achieved promising results for simple properties; its effectiveness for more complicated nested properties, however, remains unknown. This thesis presents the first systematic framework of ATPG-based BMC capable of checking properties in all nested forms on gate level. The negation counterpart to a property is mapped into a structural monitor, which is tailored to a flattened model of the input circuit. A target fault is then injected at the monitor output, and a modified ATPG-based state justification algorithm is used to search a test for this fault. Finding such a test corresponds to formally establishing the property. The framework can easily incorporate any existing ATPG tool with little modification. The proposed framework has been implemented in a computer program called FORMAL, and has been used to check a comprehensive set of properties of GL85 microprocessor and USB 2.0 circuits. Experimental results show that the ATPG-based approach performs better in both capacity and efficiency than the SAT-based techniques, especially for large bounds and for properties that require large search space. Therefore, ATPG-based BMC has been demonstrated an effective supplement to SAT-based BMC in VLSI circuit verification.

Committee: Daniel Saab (Advisor) Subjects:

Doctor of Philosophy (Ph.D.), Bowling Green State University, 2006, Mathematics/Mathematical Statistics

Item Response Theory (IRT) models are commonly used in educational and psychological testing. These models are mainly used to assess the latent abilities of examinees and the effectiveness of the test items in measuring this underlying trait. However, model checking in Item Response Theory is still an underdeveloped area. In this dissertation, various model checking strategies from a Bayesian perspective for different Item Response models are presented. In particular, three methods are employed to assess the goodness-of-fit of different IRT models. First, Bayesian residuals and different residual plots are introduced to serve as graphical procedures to check for model fit and to detect outlying items and examinees. Second, the idea of predictive distributions is used to construct reference distributions for different test quantities and discrepancy measures, including the standard deviation of point bi-serial correlations, Bock's Pearson-type chi-square index, Yen's Q1 index, Hosmer-Lemeshow Statistic, Mckinley and Mill's G2 index, Orlando and Thissen's S-G2 and S-X2 indices, Wright and Stone's W-statistic, and the Log-likelihood statistic. The prior, posterior, and partial posterior predictive distributions are discussed and employed. Finally, Bayes factor are used to compare different IRT models in model selection and detection of outlying discrimination parameters. In this topic, different numerical procedures to estimate the Bayes factors for these models are discussed. All of these proposed methods are illustrated using simulated data and Mathematics placement exam data from BGSU.

Committee: James Albert (Advisor) Subjects: