Matching Items (293)
Description
In this dissertation, two problems are addressed in the verification and control of Cyber-Physical Systems (CPS):
1) Falsification: given a CPS, and a property of interest that the CPS must satisfy under all allowed operating conditions, does the CPS violate, i.e. falsify, the property?
2) Conformance testing: given a model of a CPS, and an implementation of that CPS on an embedded platform, how can we characterize the properties satisfied by the implementation, given the properties satisfied by the model?
Both problems arise in the context of Model-Based Design (MBD) of CPS: in MBD, the designers start from a set of formal requirements that the system-to-be-designed must satisfy.
A first model of the system is created.
Because it may not be possible to formally verify the CPS model against the requirements, falsification tries to verify whether the model satisfies the requirements by searching for behavior that violates them.
In the first part of this dissertation, I present improved methods for finding falsifying behaviors of CPS when properties are expressed in Metric Temporal Logic (MTL).
These methods leverage the notion of robust semantics of MTL formulae: if a falsifier exists, it is in the neighborhood of local minimizers of the robustness function.
The proposed algorithms compute descent directions of the robustness function in the space of initial conditions and input signals, and provably converge to local minima of the robustness function.
The initial model of the CPS is then iteratively refined by modeling previously ignored phenomena, adding more functionality, etc., with each refinement resulting in a new model.
Many of the refinements in the MBD process described above do not provide an a priori guaranteed relation between the successive models.
Thus, the second problem above arises: how to quantify the distance between two successive models M_n and M_{n+1}?
If M_n has been verified to satisfy the specification, can it be guaranteed that M_{n+1} also satisfies the same, or some closely related, specification?
This dissertation answers both questions for a general class of CPS, and properties expressed in MTL.
1) Falsification: given a CPS, and a property of interest that the CPS must satisfy under all allowed operating conditions, does the CPS violate, i.e. falsify, the property?
2) Conformance testing: given a model of a CPS, and an implementation of that CPS on an embedded platform, how can we characterize the properties satisfied by the implementation, given the properties satisfied by the model?
Both problems arise in the context of Model-Based Design (MBD) of CPS: in MBD, the designers start from a set of formal requirements that the system-to-be-designed must satisfy.
A first model of the system is created.
Because it may not be possible to formally verify the CPS model against the requirements, falsification tries to verify whether the model satisfies the requirements by searching for behavior that violates them.
In the first part of this dissertation, I present improved methods for finding falsifying behaviors of CPS when properties are expressed in Metric Temporal Logic (MTL).
These methods leverage the notion of robust semantics of MTL formulae: if a falsifier exists, it is in the neighborhood of local minimizers of the robustness function.
The proposed algorithms compute descent directions of the robustness function in the space of initial conditions and input signals, and provably converge to local minima of the robustness function.
The initial model of the CPS is then iteratively refined by modeling previously ignored phenomena, adding more functionality, etc., with each refinement resulting in a new model.
Many of the refinements in the MBD process described above do not provide an a priori guaranteed relation between the successive models.
Thus, the second problem above arises: how to quantify the distance between two successive models M_n and M_{n+1}?
If M_n has been verified to satisfy the specification, can it be guaranteed that M_{n+1} also satisfies the same, or some closely related, specification?
This dissertation answers both questions for a general class of CPS, and properties expressed in MTL.
ContributorsAbbas, Houssam Y (Author) / Fainekos, Georgios (Thesis advisor) / Duman, Tolga (Thesis advisor) / Mittelmann, Hans (Committee member) / Tsakalis, Konstantinos (Committee member) / Arizona State University (Publisher)
Created2015
Description
Distributed wireless sensor networks (WSNs) have attracted researchers recently due to their advantages such as low power consumption, scalability and robustness to link failures. In sensor networks with no fusion center, consensus is a process where
all the sensors in the network achieve global agreement using only local transmissions. In this dissertation, several consensus and consensus-based algorithms in WSNs are studied.
Firstly, a distributed consensus algorithm for estimating the maximum and minimum value of the initial measurements in a sensor network in the presence of communication noise is proposed. In the proposed algorithm, a soft-max approximation together with a non-linear average consensus algorithm is used. A design parameter controls the trade-off between the soft-max error and convergence speed. An analysis of this trade-off gives guidelines towards how to choose the design parameter for the max estimate. It is also shown that if some prior knowledge of the initial measurements is available, the consensus process can be accelerated.
Secondly, a distributed system size estimation algorithm is proposed. The proposed algorithm is based on distributed average consensus and L2 norm estimation. Different sources of error are explicitly discussed, and the distribution of the final estimate is derived. The CRBs for system size estimator with average and max consensus strategies are also considered, and different consensus based system size estimation approaches are compared.
Then, a consensus-based network center and radius estimation algorithm is described. The center localization problem is formulated as a convex optimization problem with a summation form by using soft-max approximation with exponential functions. Distributed optimization methods such as stochastic gradient descent and diffusion adaptation are used to estimate the center. Then, max consensus is used to compute the radius of the network area.
Finally, two average consensus based distributed estimation algorithms are introduced: distributed degree distribution estimation algorithm and algorithm for tracking the dynamics of the desired parameter. Simulation results for all proposed algorithms are provided.
all the sensors in the network achieve global agreement using only local transmissions. In this dissertation, several consensus and consensus-based algorithms in WSNs are studied.
Firstly, a distributed consensus algorithm for estimating the maximum and minimum value of the initial measurements in a sensor network in the presence of communication noise is proposed. In the proposed algorithm, a soft-max approximation together with a non-linear average consensus algorithm is used. A design parameter controls the trade-off between the soft-max error and convergence speed. An analysis of this trade-off gives guidelines towards how to choose the design parameter for the max estimate. It is also shown that if some prior knowledge of the initial measurements is available, the consensus process can be accelerated.
Secondly, a distributed system size estimation algorithm is proposed. The proposed algorithm is based on distributed average consensus and L2 norm estimation. Different sources of error are explicitly discussed, and the distribution of the final estimate is derived. The CRBs for system size estimator with average and max consensus strategies are also considered, and different consensus based system size estimation approaches are compared.
Then, a consensus-based network center and radius estimation algorithm is described. The center localization problem is formulated as a convex optimization problem with a summation form by using soft-max approximation with exponential functions. Distributed optimization methods such as stochastic gradient descent and diffusion adaptation are used to estimate the center. Then, max consensus is used to compute the radius of the network area.
Finally, two average consensus based distributed estimation algorithms are introduced: distributed degree distribution estimation algorithm and algorithm for tracking the dynamics of the desired parameter. Simulation results for all proposed algorithms are provided.
ContributorsZhang, Sai (Electrical engineer) (Author) / Tepedelenlioğlu, Cihan (Thesis advisor) / Spanias, Andreas (Thesis advisor) / Tsakalis, Kostas (Committee member) / Bliss, Daniel (Committee member) / Arizona State University (Publisher)
Created2017
Description
The thesis explores the avenues of machine learning principles in object detection using TensorFlow 2 Object Detection API Libraries for implementation. Integrating object detection capabilities into ESP-32 cameras can enhance functionality in the capstone dragster application and potential applications, such as autonomous robots. The research implements the TensorFlow 2 Object Detection API, a widely used framework for training and deploying object detection models. By leveraging the pre-trained models available in the API, the system can detect a wide range of objects with high accuracy and speed. Fine-tuning these models using a custom dataset allows us to enhance their performance in detecting specific objects of interest. Experiments to identify strengths and weaknesses of each model's implementation before and after training using similar images were evaluated The thesis also explores the potential limitations and challenges of deploying object detection on real-time ESP-32 cameras, such as limited computational resources, costs, and power constraints. The results obtained from the experiments demonstrate the feasibility and effectiveness of implementing object detection on ESP-32 cameras using the TensorFlow2 Object Detection API. The system achieves satisfactory accuracy and real-time processing capabilities, making it suitable for various practical applications. Overall, this thesis provides a foundation for further advancements and optimizations in the integration of object detection capabilities into small, low-power devices such as ESP-32 cameras and a crossroad to explore its applicability for other image-capturing and processing devices in industrial, automotive, and defense sectors of industry.
ContributorsMani, Vinesh (Author) / Tsakalis, Konstantinos (Thesis director) / Jayasuriya, Suren (Committee member) / Barrett, The Honors College (Contributor) / Electrical Engineering Program (Contributor)
Created2024-05