Test-based falsification and conformance testing for cyber-physical systems

153597-Thumbnail Image.png
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.

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.
Date Created
2015
Agent

A new machine learning based approach to NASA's propulsion engine diagnostic benchmark problem

153567-Thumbnail Image.png
Description
Gas turbine engine for aircraft propulsion represents one of the most physics-complex and safety-critical systems in the world. Its failure diagnostic is challenging due to the complexity of the model system, difficulty involved in practical testing and the infeasibility of

Gas turbine engine for aircraft propulsion represents one of the most physics-complex and safety-critical systems in the world. Its failure diagnostic is challenging due to the complexity of the model system, difficulty involved in practical testing and the infeasibility of creating homogeneous diagnostic performance evaluation criteria for the diverse engine makes.

NASA has designed and publicized a standard benchmark problem for propulsion engine gas path diagnostic that enables comparisons among different engine diagnostic approaches. Some traditional model-based approaches and novel purely data-driven approaches such as machine learning, have been applied to this problem.

This study focuses on a different machine learning approach to the diagnostic problem. Some most common machine learning techniques, such as support vector machine, multi-layer perceptron, and self-organizing map are used to help gain insight into the different engine failure modes from the perspective of big data. They are organically integrated to achieve good performance based on a good understanding of the complex dataset.

The study presents a new hierarchical machine learning structure to enhance classification accuracy in NASA's engine diagnostic benchmark problem. The designed hierarchical structure produces an average diagnostic accuracy of 73.6%, which outperforms comparable studies that were most recently published.
Date Created
2015
Agent

Account for Uncertainty with Robust Control Design: Part 1

129453-Thumbnail Image.png
Description

Robust control design has been increasingly used in industrial settings by leading automation companies. The design procedure has evolved in the last decades and fairly automated procedures exist now for use by practicing engineers or even operators. One does not

Robust control design has been increasingly used in industrial settings by leading automation companies. The design procedure has evolved in the last decades and fairly automated procedures exist now for use by practicing engineers or even operators. One does not need to be familiar with the details of the underlying theory to use it. Robust control is different than conventional control in that it accounts for uncertainty bounds and designs a controller with known/desired performance and stability characteristics. Robust control can be applied to multivariable or Single Input Single Output (SISO) processes. This paper is aimed at providing a tutorial on the Robust PID control design approach to practicing chemical engineers. We use the classical pH control problem as an example, which is a challenging problem due to its non-linearity. First, we analyze the pH process by using the benchmark model of Henson and Seborg. We identify the fundamental limitations of the linear control design in terms of model uncertainty and sensor sampling constraints. Subsequently, we design a controller following the guidelines from robust control theory. Finally, we demonstrate the results though implementation in a lab-scale wastewater system. The experimental results show the validity of the process model and the control design approach. It also points out the limitations of the linear controller performance, leading to an interesting follow-up work regarding gain scheduling and adaptation.

Date Created
2014-11-01
Agent

Exploring latent structure in data: algorithms and implementations

153223-Thumbnail Image.png
Description
Feature representations for raw data is one of the most important component in a machine learning system. Traditionally, features are \textit{hand crafted} by domain experts which can often be a time consuming process. Furthermore, they do not generalize well to

Feature representations for raw data is one of the most important component in a machine learning system. Traditionally, features are \textit{hand crafted} by domain experts which can often be a time consuming process. Furthermore, they do not generalize well to unseen data and novel tasks. Recently, there have been many efforts to generate data-driven representations using clustering and sparse models. This dissertation focuses on building data-driven unsupervised models for analyzing raw data and developing efficient feature representations.

Simultaneous segmentation and feature extraction approaches for silicon-pores sensor data are considered. Aggregating data into a matrix and performing low rank and sparse matrix decompositions with additional smoothness constraints are proposed to solve this problem. Comparison of several variants of the approaches and results for signal de-noising and translocation/trapping event extraction are presented. Algorithms to improve transform-domain features for ion-channel time-series signals based on matrix completion are presented. The improved features achieve better performance in classification tasks and in reducing the false alarm rates when applied to analyte detection.

Developing representations for multimedia is an important and challenging problem with applications ranging from scene recognition, multi-media retrieval and personal life-logging systems to field robot navigation. In this dissertation, we present a new framework for feature extraction for challenging natural environment sounds. Proposed features outperform traditional spectral features on challenging environmental sound datasets. Several algorithms are proposed that perform supervised tasks such as recognition and tag annotation. Ensemble methods are proposed to improve the tag annotation process.

To facilitate the use of large datasets, fast implementations are developed for sparse coding, the key component in our algorithms. Several strategies to speed-up Orthogonal Matching Pursuit algorithm using CUDA kernel on a GPU are proposed. Implementations are also developed for a large scale image retrieval system. Image-based "exact search" and "visually similar search" using the image patch sparse codes are performed. Results demonstrate large speed-up over CPU implementations and good retrieval performance is also achieved.
Date Created
2014
Agent

A double grounded transformerless photovoltaic array string inverter with film capacitors and silicon carbide transistors

152908-Thumbnail Image.png
Description
A new photovoltaic (PV) array power converter circuit is presented. The salient features of this inverter are: transformerless topology, grounded PV array, and only film capacitors. The motivations are to reduce cost, eliminate leakage ground currents, and improve reliability. The

A new photovoltaic (PV) array power converter circuit is presented. The salient features of this inverter are: transformerless topology, grounded PV array, and only film capacitors. The motivations are to reduce cost, eliminate leakage ground currents, and improve reliability. The use of Silicon Carbide (SiC) transistors is the key enabling technology for this particular circuit to attain good efficiency.

Traditionally, grid connected PV inverters required a transformer for isolation and safety. The disadvantage of high frequency transformer based inverters is complexity and cost. Transformerless inverters have become more popular recently, although they can be challenging to implement because of possible high frequency currents through the PV array's stay capacitance to earth ground. Conventional PV inverters also typically utilize electrolytic capacitors for bulk power buffering. However such capacitors can be prone to decreased reliability.

The solution proposed here to solve these problems is a bi directional buck boost converter combined with half bridge inverters. This configuration enables grounding of the array's negative terminal and passive power decoupling with only film capacitors.

Several aspects of the proposed converter are discussed. First a literature review is presented on the issues to be addressed. The proposed circuit is then presented and examined in detail. This includes theory of operation, component selection, and control systems. An efficiency analysis is also conducted. Simulation results are then presented that show correct functionality. A hardware prototype is built and experiment results also prove the concept. Finally some further developments are mentioned.

As a summary of the research a new topology and control technique were developed. The resultant circuit is a high performance transformerless PV inverter with upwards of 97% efficiency.
Date Created
2014
Agent

Some applications of vector fitting in the solution of electromagnetic fields and interactions

152406-Thumbnail Image.png
Description
Vector Fitting (VF) is a recent macromodeling method that has been popularized by its use in many commercial software for extracting equivalent circuit's of simulated networks. Specifically for material measurement applications, VF is shown to estimate either the permittivity or

Vector Fitting (VF) is a recent macromodeling method that has been popularized by its use in many commercial software for extracting equivalent circuit's of simulated networks. Specifically for material measurement applications, VF is shown to estimate either the permittivity or permeability of a multi-Debye material accurately, even when measured in the presence of noise and interferences caused by test setup imperfections. A brief history and survey of methods utilizing VF for material measurement will be introduced in this work. It is shown how VF is useful for macromodeling dielectric materials after being measured with standard transmission line and free-space methods. The sources of error in both an admittance tunnel test device and stripline resonant cavity test device are identified and VF is employed for correcting these errors. Full-wave simulations are performed to model the test setup imperfections and the sources of interference they cause are further verified in actual hardware measurements. An accurate macromodel is attained as long as the signal-to-interference-ratio (SIR) in the measurement is sufficiently high such that the Debye relaxations are observable in the data. Finally, VF is applied for macromodeling the time history of the total fields scattering from a perfectly conducting wedge. This effort is an initial test to see if a time domain theory of diffraction exists, and if the diffraction coefficients may be exactly modeled with VF. This section concludes how VF is not only useful for applications in material measurement, but for the solution of modeling fields and interactions in general.
Date Created
2013
Agent

Towards adaptive micro-robotic neural interfaces: autonomous navigation of microelectrodes in the brain for optimal neural recording

152400-Thumbnail Image.png
Description
Advances in implantable MEMS technology has made possible adaptive micro-robotic implants that can track and record from single neurons in the brain. Development of autonomous neural interfaces opens up exciting possibilities of micro-robots performing standard electrophysiological techniques that would previously

Advances in implantable MEMS technology has made possible adaptive micro-robotic implants that can track and record from single neurons in the brain. Development of autonomous neural interfaces opens up exciting possibilities of micro-robots performing standard electrophysiological techniques that would previously take researchers several hundred hours to train and achieve the desired skill level. It would result in more reliable and adaptive neural interfaces that could record optimal neural activity 24/7 with high fidelity signals, high yield and increased throughput. The main contribution here is validating adaptive strategies to overcome challenges in autonomous navigation of microelectrodes inside the brain. The following issues pose significant challenges as brain tissue is both functionally and structurally dynamic: a) time varying mechanical properties of the brain tissue-microelectrode interface due to the hyperelastic, viscoelastic nature of brain tissue b) non-stationarities in the neural signal caused by mechanical and physiological events in the interface and c) the lack of visual feedback of microelectrode position in brain tissue. A closed loop control algorithm is proposed here for autonomous navigation of microelectrodes in brain tissue while optimizing the signal-to-noise ratio of multi-unit neural recordings. The algorithm incorporates a quantitative understanding of constitutive mechanical properties of soft viscoelastic tissue like the brain and is guided by models that predict stresses developed in brain tissue during movement of the microelectrode. An optimal movement strategy is developed that achieves precise positioning of microelectrodes in the brain by minimizing the stresses developed in the surrounding tissue during navigation and maximizing the speed of movement. Results of testing the closed-loop control paradigm in short-term rodent experiments validated that it was possible to achieve a consistently high quality SNR throughout the duration of the experiment. At the systems level, new generation of MEMS actuators for movable microelectrode array are characterized and the MEMS device operation parameters are optimized for improved performance and reliability. Further, recommendations for packaging to minimize the form factor of the implant; design of device mounting and implantation techniques of MEMS microelectrode array to enhance the longevity of the implant are also included in a top-down approach to achieve a reliable brain interface.
Date Created
2013
Agent

Feedback control and obstacle avoidance for non-holonomic differential drive robots

152330-Thumbnail Image.png
Description
This thesis discusses control and obstacle avoidance for non-holonomic differential drive mobile vehicles. The two important behaviors for the vehicle can be defined as go to goal and obstacle avoidance behavior. This thesis discusses both behaviors in detail. Go to

This thesis discusses control and obstacle avoidance for non-holonomic differential drive mobile vehicles. The two important behaviors for the vehicle can be defined as go to goal and obstacle avoidance behavior. This thesis discusses both behaviors in detail. Go to goal behavior is the ability of the mobile vehicle to go from one particular co-ordinate to another. Cruise control, cartesian and posture stabilization problems are discussed as the part of this behavior. Control strategies used for the above three problems are explained in the thesis. Matlab simulations are presented to verify these controllers. Obstacle avoidance behavior ensures that the vehicle doesn't hit object in its path while going towards the goal. Three different techniques for obstacle avoidance which are useful for different kind of obstacles are described in the thesis. Matlab simulations are presented to show and discuss the three techniques. The controls discussed for the cartesian and posture stabilization were implemented on a low cost miniature vehicle to verify the results practically. The vehicle is described in the thesis in detail. The practical results are compared with the simulations. Hardware and matlab codes have been provided as a reference for the reader.
Date Created
2013
Agent

Non-holonomic differential drive mobile robot control & design: critical dynamics and coupling constraints

152311-Thumbnail Image.png
Description
Mobile robots are used in a broad range of application areas; e.g. search and rescue, reconnaissance, exploration, etc. Given the increasing need for high performance mobile robots, the area has received attention by researchers. In this thesis, critical control and

Mobile robots are used in a broad range of application areas; e.g. search and rescue, reconnaissance, exploration, etc. Given the increasing need for high performance mobile robots, the area has received attention by researchers. In this thesis, critical control and control-relevant design issues for differential drive mobile robots is addressed. Two major themes that have been explored are the use of kinematic models for control design and the use of decentralized proportional plus integral (PI) control. While these topics have received much attention, there still remain critical questions which have not been rigorously addressed. In this thesis, answers to the following critical questions are provided: When is 1. a kinematic model sufficient for control design? 2. coupled dynamics essential? 3. a decentralized PI inner loop velocity controller sufficient? 4. centralized multiple-input multiple-output (MIMO) control essential? and how can one design the robot to relax the requirements implied in 1 and 2? In this thesis, the following is shown: 1. The nonlinear kinematic model will suffice for control design when the inner velocity (dynamic) loop is much faster (10X) than the slower outer positioning loop. 2. A dynamic model is essential when the inner velocity (dynamic) loop is less than two times faster than the slower outer positioning loop. 3. A decentralized inner loop PI velocity controller will be sufficient for accomplish- ing high performance control when the required velocity bandwidth is small, rel- ative to the peak dynamic coupling frequency. A rule-of-thumb which depends on the robot aspect ratio is given. 4. A centralized MIMO velocity controller is needed when the required bandwidth is large, relative to the peak dynamic coupling frequency. Here, the analysis in the thesis is sparse making the topic an area for future analytical work. Despite this, it is clearly shown that a centralized MIMO inner loop controller can offer increased performance vis- ́a-vis a decentralized PI controller. 5. Finally, it is shown how the dynamic coupling depends on the robot aspect ratio and how the coupling can be significantly reduced. As such, this can be used to ease the requirements imposed by 2 and 4 above.
Date Created
2013
Agent

A study on constrained state estimators

152273-Thumbnail Image.png
Description
This study focuses on state estimation of nonlinear discrete time systems with constraints. Physical processes have inherent in them, constraints on inputs, outputs, states and disturbances. These constraints can provide additional information to the estimator in estimating states from the

This study focuses on state estimation of nonlinear discrete time systems with constraints. Physical processes have inherent in them, constraints on inputs, outputs, states and disturbances. These constraints can provide additional information to the estimator in estimating states from the measured output. Recursive filters such as Kalman Filters or Extended Kalman Filters are commonly used in state estimation; however, they do not allow inclusion of constraints in their formulation. On the other hand, computational complexity of full information estimation (using all measurements) grows with iteration and becomes intractable. One way of formulating the recursive state estimation problem with constraints is the Moving Horizon Estimation (MHE) approximation. Estimates of states are calculated from the solution of a constrained optimization problem of fixed size. Detailed formulation of this strategy is studied and properties of this estimation algorithm are discussed in this work. The problem with the MHE formulation is solving an optimization problem in each iteration which is computationally intensive. State estimation with constraints can be formulated as Extended Kalman Filter (EKF) with a projection applied to estimates. The states are estimated from the measurements using standard Extended Kalman Filter (EKF) algorithm and the estimated states are projected on to a constrained set. Detailed formulation of this estimation strategy is studied and the properties associated with this algorithm are discussed. Both these state estimation strategies (MHE and EKF with projection) are tested with examples from the literature. The average estimation time and the sum of square estimation error are used to compare performance of these estimators. Results of the case studies are analyzed and trade-offs are discussed.
Date Created
2013
Agent