Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Publication
- Publication Type
Articles 1 - 5 of 5
Full-Text Articles in Physical Sciences and Mathematics
Representation And Reconstruction Of Linear, Time-Invariant Networks, Nathan Scott Woodbury
Representation And Reconstruction Of Linear, Time-Invariant Networks, Nathan Scott Woodbury
Theses and Dissertations
Network reconstruction is the process of recovering a unique structured representation of some dynamic system using input-output data and some additional knowledge about the structure of the system. Many network reconstruction algorithms have been proposed in recent years, most dealing with the reconstruction of strictly proper networks (i.e., networks that require delays in all dynamics between measured variables). However, no reconstruction technique presently exists capable of recovering both the structure and dynamics of networks where links are proper (delays in dynamics are not required) and not necessarily strictly proper.The ultimate objective of this dissertation is to develop algorithms capable of …
Verifying Abstract Components Within Concrete Software Environments, Tonglaga Bao
Verifying Abstract Components Within Concrete Software Environments, Tonglaga Bao
Theses and Dissertations
In order to model check a software component which is not a standalone program, we need a model of the software which completes the program. This problem is important for software engineers who need to deploy an existing component into a new environment. The model is typically generated by abstracting the surrounding software environment in which the component will be executed. However, abstracting the surrounding software is a difficult and error-prone task, particularly when the surrounding software is a complex software artifact which can not be easily abstracted. In this dissertation, we present a new approach to the problem by …
On-The-Fly Dynamic Dead Variable Analysis, Joel P. Self
On-The-Fly Dynamic Dead Variable Analysis, Joel P. Self
Theses and Dissertations
State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover …
Dynamic Dead Variable Analysis, Micah S. Lewis
Dynamic Dead Variable Analysis, Micah S. Lewis
Theses and Dissertations
Dynamic dead variable analysis (DDVA) extends traditional static dead variable analysis (SDVA) in the context of model checking through the use of run-time information. The analysis is run multiple times during the course of model checking to create a more precise set of dead variables. The DDVA is evaluated based on the amount of memory used to complete model checking relative to SDVA while considering the extra overhead required to implement DDVA. On several models with a complex control flow graph, DDVA reduces the amount of memory needed by 38-88MB compared to SDVA with a cost of 36 bytes of …
Modular Verification Of Timed Circuits Using Automatic Abstraction, Eric G. Mercer, Chris Myers, Hao Zheng
Modular Verification Of Timed Circuits Using Automatic Abstraction, Eric G. Mercer, Chris Myers, Hao Zheng
Faculty Publications
The major barrier that prevents the application of formal verification to large designs is state explosion. This paper presents a new approach for verification of timed circuits using automatic abstraction. This approach partitions the design into modules, each with constrained complexity. Before verification is applied to each individual module, irrelevant information to the behavior of the selected module is abstracted away. This approach converts a verification problem with big exponential complexity to a set of subproblems, each with small exponential complexity. Experimental results are promising in that they indicate that our approach has the potential of completing much faster while …