Matching Items (71)
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
Vertical taking off and landing (VTOL) drones started to emerge at the beginning of this century, and finds applications in the vast areas of mapping, rescuing, logistics, etc. Usually a VTOL drone control system design starts from a first principles model. Most of the VTOL drones are in the shape of a quad-rotor which is convenient for dynamic analysis.
In this project, a VTOL drone with shape similar to a Convair XFY-1 is studied and the primary focus is developing and examining an alternative method to identify a system model from the input and output data, with which it is possible to estimate system parameters and compute model uncertainties on discontinuous data sets. We verify the models by designing controllers that stabilize the yaw, pitch, and roll angles for the VTOL drone in the hovering state.
This project comprises of three stages: an open-loop identification to identify the yaw and pitch dynamics, an intermediate closed-loop identification to identify the roll action dynamic and a closed-loop identification to refine the identification of yaw and pitch action. In open and closed loop identifications, the reference signals sent to the servos were recorded as inputs to the system and the angles and angular velocities in yaw and pitch directions read by inertial measurement unit were recorded as outputs of the system. In the intermediate closed loop identification, the difference between the reference signals sent to the motors on the contra-rotators was recorded as input and the roll angular velocity is recorded as output. Next, regressors were formed by using a coprime factor structure and then parameters of the system were estimated using the least square method. Multiplicative and divisive uncertainties were calculated from the data set and were used to guide PID loop-shaping controller design.
In this project, a VTOL drone with shape similar to a Convair XFY-1 is studied and the primary focus is developing and examining an alternative method to identify a system model from the input and output data, with which it is possible to estimate system parameters and compute model uncertainties on discontinuous data sets. We verify the models by designing controllers that stabilize the yaw, pitch, and roll angles for the VTOL drone in the hovering state.
This project comprises of three stages: an open-loop identification to identify the yaw and pitch dynamics, an intermediate closed-loop identification to identify the roll action dynamic and a closed-loop identification to refine the identification of yaw and pitch action. In open and closed loop identifications, the reference signals sent to the servos were recorded as inputs to the system and the angles and angular velocities in yaw and pitch directions read by inertial measurement unit were recorded as outputs of the system. In the intermediate closed loop identification, the difference between the reference signals sent to the motors on the contra-rotators was recorded as input and the roll angular velocity is recorded as output. Next, regressors were formed by using a coprime factor structure and then parameters of the system were estimated using the least square method. Multiplicative and divisive uncertainties were calculated from the data set and were used to guide PID loop-shaping controller design.
ContributorsLiu, Yiqiu (Author) / Tsakalis, Konstantinos (Thesis advisor) / Rodriguez, Armando (Thesis advisor) / Rivera, Daniel (Committee member) / Arizona State University (Publisher)
Created2015
Description
Buck converters are electronic devices that changes a voltage from one level to a lower one and are present in many everyday applications. However, due to factors like aging, degradation or failures, these devices require a system identification process to track and diagnose their parameters. The system identification process should be performed on-line to not affect the normal operation of the device. Identifying the parameters of the system is essential to design and tune an adaptive proportional-integral-derivative (PID) controller.
Three techniques were used to design the PID controller. Phase and gain margin still prevails as one of the easiest methods to design controllers. Pole-zero cancellation is another technique which is based on pole-placement. However, although these controllers can be easily designed, they did not provide the best response compared to the Frequency Loop Shaping (FLS) technique. Therefore, since FLS showed to have a better frequency and time responses compared to the other two controllers, it was selected to perform the adaptation of the system.
An on-line system identification process was performed for the buck converter using indirect adaptation and the least square algorithm. The estimation error and the parameter error were computed to determine the rate of convergence of the system. The indirect adaptation required about 2000 points to converge to the true parameters prior designing the controller. These results were compared to the adaptation executed using robust stability condition (RSC) and a switching controller. Two different scenarios were studied consisting of five plants that defined the percentage of deterioration of the capacitor and inductor within the buck converter. The switching logic did not always select the optimal controller for the first scenario because the frequency response of the different plants was not significantly different. However, the second scenario consisted of plants with more noticeable different frequency responses and the switching logic selected the optimal controller all the time in about 500 points. Additionally, a disturbance was introduced at the plant input to observe its effect in the switching controller. However, for reasonable low disturbances no change was detected in the proper selection of controllers.
Three techniques were used to design the PID controller. Phase and gain margin still prevails as one of the easiest methods to design controllers. Pole-zero cancellation is another technique which is based on pole-placement. However, although these controllers can be easily designed, they did not provide the best response compared to the Frequency Loop Shaping (FLS) technique. Therefore, since FLS showed to have a better frequency and time responses compared to the other two controllers, it was selected to perform the adaptation of the system.
An on-line system identification process was performed for the buck converter using indirect adaptation and the least square algorithm. The estimation error and the parameter error were computed to determine the rate of convergence of the system. The indirect adaptation required about 2000 points to converge to the true parameters prior designing the controller. These results were compared to the adaptation executed using robust stability condition (RSC) and a switching controller. Two different scenarios were studied consisting of five plants that defined the percentage of deterioration of the capacitor and inductor within the buck converter. The switching logic did not always select the optimal controller for the first scenario because the frequency response of the different plants was not significantly different. However, the second scenario consisted of plants with more noticeable different frequency responses and the switching logic selected the optimal controller all the time in about 500 points. Additionally, a disturbance was introduced at the plant input to observe its effect in the switching controller. However, for reasonable low disturbances no change was detected in the proper selection of controllers.
ContributorsSerrano Rodriguez, Victoria Melissa (Author) / Tsakalis, Konstantinos (Thesis advisor) / Bakkaloglu, Bertan (Thesis advisor) / Rodriguez, Armando (Committee member) / Spanias, Andreas (Committee member) / Arizona State University (Publisher)
Created2016
Description
For a sensor array, part of its elements may fail to work due to hardware failures. Then the missing data may distort in the beam pattern or decrease the accuracy of direction-of-arrival (DOA) estimation. Therefore, considerable research has been conducted to develop algorithms that can estimate the missing signal information. On the other hand, through those algorithms, array elements can also be selectively turned off while the missed information can be successfully recovered, which will save power consumption and hardware cost.
Conventional approaches focusing on array element failures are mainly based on interpolation or sequential learning algorithm. Both of them rely heavily on some prior knowledge such as the information of the failures or a training dataset without missing data. In addition, since most of the existing approaches are developed for DOA estimation, their recovery target is usually the co-variance matrix but not the signal matrix.
In this thesis, a new signal recovery method based on matrix completion (MC) theory is introduced. It aims to directly refill the absent entries in the signal matrix without any prior knowledge. We proposed a novel overlapping reshaping method to satisfy the applying conditions of MC algorithms. Compared to other existing MC based approaches, our proposed method can provide us higher probability of successful recovery. The thesis describes the principle of the algorithms and analyzes the performance of this method. A few application examples with simulation results are also provided.
Conventional approaches focusing on array element failures are mainly based on interpolation or sequential learning algorithm. Both of them rely heavily on some prior knowledge such as the information of the failures or a training dataset without missing data. In addition, since most of the existing approaches are developed for DOA estimation, their recovery target is usually the co-variance matrix but not the signal matrix.
In this thesis, a new signal recovery method based on matrix completion (MC) theory is introduced. It aims to directly refill the absent entries in the signal matrix without any prior knowledge. We proposed a novel overlapping reshaping method to satisfy the applying conditions of MC algorithms. Compared to other existing MC based approaches, our proposed method can provide us higher probability of successful recovery. The thesis describes the principle of the algorithms and analyzes the performance of this method. A few application examples with simulation results are also provided.
ContributorsFan, Jie (Author) / Spanias, Andreas (Thesis advisor) / Tepedelenlioğlu, Cihan (Committee member) / Tsakalis, Konstantinos (Committee member) / Arizona State University (Publisher)
Created2016
Description
From time immemorial, epilepsy has persisted to be one of the greatest impediments to human life for those stricken by it. As the fourth most common neurological disorder, epilepsy causes paroxysmal electrical discharges in the brain that manifest as seizures. Seizures have the effect of debilitating patients on a physical and psychological level. Although not lethal by themselves, they can bring about total disruption in consciousness which can, in hazardous conditions, lead to fatality. Roughly 1\% of the world population suffer from epilepsy and another 30 to 50 new cases per 100,000 increase the number of affected annually. Controlling seizures in epileptic patients has therefore become a great medical and, in recent years, engineering challenge.
In this study, the conditions of human seizures are recreated in an animal model of temporal lobe epilepsy. The rodents used in this study are chemically induced to become chronically epileptic. Their Electroencephalogram (EEG) data is then recorded and analyzed to detect and predict seizures; with the ultimate goal being the control and complete suppression of seizures.
Two methods, the maximum Lyapunov exponent and the Generalized Partial Directed Coherence (GPDC), are applied on EEG data to extract meaningful information. Their effectiveness have been reported in the literature for the purpose of prediction of seizures and seizure focus localization. This study integrates these measures, through some modifications, to robustly detect seizures and separately find precursors to them and in consequence provide stimulation to the epileptic brain of rats in order to suppress seizures. Additionally open-loop stimulation with biphasic currents of various pairs of sites in differing lengths of time have helped us create control efficacy maps. While GPDC tells us about the possible location of the focus, control efficacy maps tells us how effective stimulating a certain pair of sites will be.
The results from computations performed on the data are presented and the feasibility of the control problem is discussed. The results show a new reliable means of seizure detection even in the presence of artifacts in the data. The seizure precursors provide a means of prediction, in the order of tens of minutes, prior to seizures. Closed loop stimulation experiments based on these precursors and control efficacy maps on the epileptic animals show a maximum reduction of seizure frequency by 24.26\% in one animal and reduction of length of seizures by 51.77\% in another. Thus, through this study it was shown that the implementation of the methods can ameliorate seizures in an epileptic patient. It is expected that the new knowledge and experimental techniques will provide a guide for future research in an effort to ultimately eliminate seizures in epileptic patients.
In this study, the conditions of human seizures are recreated in an animal model of temporal lobe epilepsy. The rodents used in this study are chemically induced to become chronically epileptic. Their Electroencephalogram (EEG) data is then recorded and analyzed to detect and predict seizures; with the ultimate goal being the control and complete suppression of seizures.
Two methods, the maximum Lyapunov exponent and the Generalized Partial Directed Coherence (GPDC), are applied on EEG data to extract meaningful information. Their effectiveness have been reported in the literature for the purpose of prediction of seizures and seizure focus localization. This study integrates these measures, through some modifications, to robustly detect seizures and separately find precursors to them and in consequence provide stimulation to the epileptic brain of rats in order to suppress seizures. Additionally open-loop stimulation with biphasic currents of various pairs of sites in differing lengths of time have helped us create control efficacy maps. While GPDC tells us about the possible location of the focus, control efficacy maps tells us how effective stimulating a certain pair of sites will be.
The results from computations performed on the data are presented and the feasibility of the control problem is discussed. The results show a new reliable means of seizure detection even in the presence of artifacts in the data. The seizure precursors provide a means of prediction, in the order of tens of minutes, prior to seizures. Closed loop stimulation experiments based on these precursors and control efficacy maps on the epileptic animals show a maximum reduction of seizure frequency by 24.26\% in one animal and reduction of length of seizures by 51.77\% in another. Thus, through this study it was shown that the implementation of the methods can ameliorate seizures in an epileptic patient. It is expected that the new knowledge and experimental techniques will provide a guide for future research in an effort to ultimately eliminate seizures in epileptic patients.
ContributorsShafique, Md Ashfaque Bin (Author) / Tsakalis, Konstantinos (Thesis advisor) / Rodriguez, Armando (Committee member) / Muthuswamy, Jitendran (Committee member) / Spanias, Andreas (Committee member) / Arizona State University (Publisher)
Created2016
Description
A nonlinear dynamic model for a passively cooled small modular reactor (SMR) is developed. The nuclear steam supply system (NSSS) model includes representations for reactor core, steam generator, pressurizer, hot leg riser and downcomer. The reactor core is modeled with the combination of: (1) neutronics, using point kinetics equations for reactor power and a single combined neutron group, and (2) thermal-hydraulics, describing the heat transfer from fuel to coolant by an overall heat transfer resistance and single-phase natural circulation. For the helical-coil once-through steam generator, a single tube depiction with time-varying boundaries and three regions, i.e., subcooled, boiling, and superheated, is adopted. The pressurizer model is developed based upon the conservation of fluid mass, volume, and energy. Hot leg riser and downcomer are treated as first-order lags. The NSSS model is incorporated with a turbine model which permits observing the power with given steam flow, pressure, and enthalpy as input. The overall nonlinear system is implemented in the Simulink dynamic environment. Simulations for typical perturbations, e.g., control rod withdrawal and increase in steam demand, are run. A detailed analysis of the results show that the steady-state values for full power are in good agreement with design data and the model is capable of predicting the dynamics of the SMR. Finally, steady-state control programs for reactor power and pressurizer pressure are also implemented and their effect on the important system variables are discussed.
ContributorsArda, Samet Egemen (Author) / Holbert, Keith E. (Thesis advisor) / Undrill, John (Committee member) / Tylavsky, Daniel (Committee member) / Karady, George G. (Committee member) / Arizona State University (Publisher)
Created2016
Description
In the recent past, due to regulatory hurdles and the inability to expand transmission systems, the bulk power system is increasingly being operated close to its limits. Among the various phenomenon encountered, static voltage stability has received increased attention among electric utilities. One approach to investigate static voltage stability is to run a set of power flow simulations and derive the voltage stability limit based on the analysis of power flow results. Power flow problems are formulated as a set of nonlinear algebraic equations usually solved by iterative methods. The most commonly used method is the Newton-Raphson method. However, at the static voltage stability limit, the Jacobian becomes singular. Hence, the power flow solution may fail to converge close to the true limit.
To carefully examine the limitations of conventional power flow software packages in determining voltage stability limits, two lines of research are pursued in this study. The first line of the research is to investigate the capability of different power flow solution techniques, such as conventional power flow and non-iterative power flow techniques to obtain the voltage collapse point. The software packages used in this study include Newton-based methods contained in PSSE, PSLF, PSAT, PowerWorld, VSAT and a non-iterative technique known as the holomorphic embedding method (HEM).
The second line is to investigate the impact of the available control options and solution parameter settings that can be utilized to obtain solutions closer to the voltage collapse point. Such as the starting point, generator reactive power limits, shunt device control modes, area interchange control, and other such parameters.
To carefully examine the limitations of conventional power flow software packages in determining voltage stability limits, two lines of research are pursued in this study. The first line of the research is to investigate the capability of different power flow solution techniques, such as conventional power flow and non-iterative power flow techniques to obtain the voltage collapse point. The software packages used in this study include Newton-based methods contained in PSSE, PSLF, PSAT, PowerWorld, VSAT and a non-iterative technique known as the holomorphic embedding method (HEM).
The second line is to investigate the impact of the available control options and solution parameter settings that can be utilized to obtain solutions closer to the voltage collapse point. Such as the starting point, generator reactive power limits, shunt device control modes, area interchange control, and other such parameters.
ContributorsYi, Weili (Author) / Vittal, Vijay (Thesis advisor) / Tylavsky, Daniel (Thesis advisor) / Qin, Jiangchao (Committee member) / Arizona State University (Publisher)
Created2017
Description
This thesis examines themodeling, analysis, and control system design issues for scramjet powered hypersonic vehicles. A nonlinear three degrees of freedom longitudinal model which includes aero-propulsion-elasticity effects was used for all analyses. This model is based upon classical compressible flow and Euler-Bernouli structural concepts. Higher fidelity computational fluid dynamics and finite element methods are needed for more precise intermediate and final evaluations. The methods presented within this thesis were shown to be useful for guiding initial control relevant design. The model was used to examine the vehicle's static and dynamic characteristics over the vehicle's trimmable region. The vehicle has significant longitudinal coupling between the fuel equivalency ratio (FER) and the flight path angle (FPA). For control system design, a two-input two-output plant (FER - elevator to speed-FPA) with 11 states (including 3 flexible modes) was used. Velocity, FPA, and pitch were assumed to be available for feedback. Aerodynamic heat modeling and design for the assumed TPS was incorporated to original Bolender's model to study the change in static and dynamic properties. De-centralized control stability, feasibility and limitations issues were dealt with the change in TPS elasticity, mass and physical dimension. The impact of elasticity due to TPS mass, TPS physical dimension as well as prolonged heating was also analyzed to understand performance limitations of de-centralized control designed for nominal model.
ContributorsKhatri, Jaidev (Author) / Rodriguez, Armando Antonio (Thesis advisor) / Tsakalis, Konstantinos (Committee member) / Wells, Valana (Committee member) / Arizona State University (Publisher)
Created2011
Description
After a power system blackout, system restoration is the most important task for the operators. Most power systems rely on an off&ndashline; restoration plan and the experience of operators to select scenarios for the black start path. Using an off&ndashline; designed restoration plan based on past experience may not be the most reliable approach under changing network configurations and loading levels. Hence, an objective restoration path selection procedure, including the option to check constraints, may be more responsive in providing directed guidance to the operators to identify the optimal transmission path to deliver power to other power plants or to pick up load as needed. After the system is subjected to a blackout, parallel restoration is an efficient way to speed up the restoration process. For a large scale power system, this system sectionalizing problem is quite complicated when considering black&ndashstart; constraints, generation/load balance constraints and voltage constraints. This dissertation presents an ordered binary decision diagram (OBDD) &ndashbased; system sectionalizing method, by which the splitting points can be quickly found. The simulation results on the IEEE 39 and 118&ndashbus; system show that the method can successfully split the system into subsystems satisfying black&ndashstart; constraints, generation/load balance constraints and voltage constraints. A power transfer distribution factor (PTDF)&ndashbased; approach will be described in this dissertation to check constraints while restoring the system. Two types of restoration performance indices are utilized considering all possible restoration paths, which are then ranked according to their expected performance characteristics as reflected by the restoration performance index. PTDFs and weighting factors are used to determine the ordered list of restoration paths, which can enable the load to be picked up by lightly loaded lines or relieve stress on heavily loaded lines. A transmission path agent can then be formulated by performing the automatic path selection under different system operating conditions. The proposed restoration strategy is tested on the IEEE&ndash39; bus system and on the Western region of the Entergy system. The testing results reveal that the proposed strategy can be used in real time.
ContributorsWang, Chong (Author) / Vittal, Vijay (Thesis advisor) / Tylavsky, Daniel (Committee member) / Heydt, Gerald (Committee member) / Farmer, Richard (Committee member) / Arizona State University (Publisher)
Created2010
Description
Localization tasks using two-way ranging (TWR) are making headway in modern daynavigation applications as an alternative to legacy global navigation satellite systems
(GNSS) such as GPS. There is not currently literature that provides a closed-form
expression for estimation performance bounds on position and attitude when a TWR
system is employed. A Cramer-Rao Lower Bounds (CRLB) is derived for position
and orientation estimation using both 2-D and 3-D geometries. A literature review is
performed to give background and detail on the tools needed for a thorough analysis of
this problem. Popular Least Squares techniques and solutions to Wahba’s problem are
compared to the derived bounds as proof of correctness using Monte Carlo simulations.
A brief exploration on estimation performance using an Extended Kalman Filter for
non-stationary users is also looked at as an introduction to future extensions to this
work. The literature Applications like the CHP2 system are discussed as well to show
how secure, inexpensive and robust implementation of TWR is highly feasible.
i
ContributorsWelker, Samuel (Author) / Bliss, Daniel (Thesis advisor) / Herschfelt, Andrew (Committee member) / Tsakalis, Konstantinos (Committee member) / Arizona State University (Publisher)
Created2022