- About
-
The Global ETD Search service is a free service for researchers
to find electronic theses and dissertations. This service is
provided by the
Networked Digital Library of Theses and Dissertations.
Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
Search results
Showing 1 to 3 of 3 (0.082 seconds)| 1 |
Hierarchical Interface-Based Decentralized Supervisory ControlLiu, Huailiang 11 December 2015 (has links)
In decentralized control, agents have only
a partial view and partial control of the system and must cooperate to
achieve the control objective. In order to synthesize a decentralized control
solution, a specification must satisfy the co-observability
property. Existing co-observability verification methods require the
possibly intractable construction of the complete system. To address
this issue, we introduce an incremental verification of
co-observability approach. Selected subgroups of the system are evaluated
individually, until verification is complete. The new method is
potentially much more efficient than the monolithic approaches, in
particular for systems composed of many subsystems, allowing for some
intractable problems to be manageable. Properties of this new strategy
are presented, along with a corresponding algorithm and an example.
To further increase the scalability of decentralized control, we wish
to adapt the existing Hierarchical Interface-Based Supervisory Control
(HISC) to support it. We introduce the Hierarchical
Interface-Based Decentralized Supervisory Control (HIDSC) framework
that extends HISC to decentralized control.
To adapt co-observability for HIDSC, we propose a per-component definition
of co-observability along with a verification strategy that requires
only a single component at a time in order to verify
co-observability. Finally, we provide and prove
the necessary and sufficient conditions for supervisory control
existence in the HIDSC framework and illustrate our approach with an
example. As the entire system model never needs to be constructed, HIDSC
potentially provides significant savings. / Thesis / Doctor of Philosophy (PhD)
|
| 2 |
Techniques to facilitate symbolic execution of real-world programsAnand, Saswat 11 May 2012 (has links)
The overall goal of this research is to reduce the cost of software development and improve the quality of software. Symbolic execution is a program-analysis technique that is used to address several problems that arise in developing high-quality software. Despite the fact that the symbolic execution technique is well understood, and performing symbolic execution on simple programs is straightforward, it is still not possible to apply the technique to the general class of large, real-world software. A symbolic-execution system can be effectively applied to large, real-world software if it has at least the two features: efficiency and automation. However, efficient and automatic symbolic execution of real-world programs is a lofty goal because of both theoretical and practical reasons. Theoretically, achieving this goal requires solving an intractable problem (i.e., solving constraints). Practically, achieving this goal requires overwhelming effort to implement a symbolic-execution system that can precisely and automatically symbolically execute real-world programs.
This research makes three major contributions.
1. Three new techniques that address three important problems of symbolic execution. Compared to existing techniques, the new techniques
* reduce the manual effort that may be required to symbolically execute those programs that either generate complex constraints or parts of which cannot be symbolically executed due to limitations of a symbolic-execution system.
* improve the usefulness of symbolic execution (e.g., expose more bugs in a program) by enabling discovery of more feasible paths within a given time budget.
2. A novel approach that uses symbolic execution to generate test inputs for Apps that run on modern mobile devices such as smartphones and tablets.
3. Implementations of the above techniques and empirical results obtained from applying those techniques to real-world programs that demonstrate their effectiveness.
|
| 3 |
On-the-Fly Dynamic Dead Variable AnalysisSelf, Joel P. 22 March 2007 (has links) (PDF)
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 variable assignments that are not used. When applied to model checking, this allows us to ignore the entire input range of dead variables and thus reduce the size of the explored state space. Prior research into dead variable analysis for model checking does not make full use of dynamic run-time information that is present during model checking. We present an algorithm for intraprocedural dead variable analysis that uses dynamic run-time information to find more dead variables on-the-fly and further reduce the size of the explored state space. We introduce a definition for the maximal state space reduction possible through an on-the-fly dead variable analysis and then show that our algorithm produces a maximal reduction in the absence of non-determinism.
|
Page generated in 0.085 seconds