Matching Items (266)
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
To ensure system integrity, robots need to proactively avoid any unwanted physical perturbation that may cause damage to the underlying hardware. In this thesis work, we investigate a machine learning approach that allows robots to anticipate impending physical perturbations from perceptual cues. In contrast to other approaches that require knowledge about sources of perturbation to be encoded before deployment, our method is based on experiential learning. Robots learn to associate visual cues with subsequent physical perturbations and contacts. In turn, these extracted visual cues are then used to predict potential future perturbations acting on the robot. To this end, we introduce a novel deep network architecture which combines multiple sub- networks for dealing with robot dynamics and perceptual input from the environment. We present a self-supervised approach for training the system that does not require any labeling of training data. Extensive experiments in a human-robot interaction task show that a robot can learn to predict physical contact by a human interaction partner without any prior information or labeling. Furthermore, the network is able to successfully predict physical contact from either depth stream input or traditional video input or using both modalities as input.
ContributorsSur, Indranil (Author) / Amor, Heni B (Thesis advisor) / Fainekos, Georgios (Committee member) / Yang, Yezhou (Committee member) / Arizona State University (Publisher)
Created2017
Description
Recent developments in computational software and public accessibility of gridded climatological data have enabled researchers to study Urban Heat Island (UHI) effects more systematically and at a higher spatial resolution. Previous studies have analyzed UHI and identified significant contributors at the regional level for cities, within the topology of urban canyons, and for different construction materials.
In UHIs, air is heated by the convective energy transfer from land surface materials and anthropogenic activities. Convection is dependent upon the temperature of the surface, temperature of the air, wind speed, and relative humidity. At the same time, air temperature is also influenced by greenhouse gases (GHG) in the atmosphere. Climatologists project a 1-5°C increase in near-surface air temperature over the next several decades, and 1-4°C specifically for Los Angeles and Maricopa during summertime due to GHG effects. With higher ambient air temperatures, we seek to understand how convection will change in cities and to what ends.
In this paper we develop a spatially explicit methodology for quantifying UHI by estimating the daily convection thermal energy transfer from land to air using publicly-available gridded climatological data, and we estimate how much additional energy will be retained due to lack of convective cooling in scenarios of higher ambient air temperature.
ContributorsBurillo, Daniel (Author) / Chester, Mikhail Vin (Author) / Kaloush, Kamil (Author) / Thau, David (Author) / Chang, Andrew (Author) / Arizona State University. School of Sustainable Engineering and the Built Environment (Contributor) / Arizona State University. Center for Earth Systems Engineering and Management (Contributor)
Description
The meta-MAC protocol is a systematic and automatic method to dynamically combine any set of existing Medium Access Control (MAC) protocols into a single higher level MAC protocol. The meta-MAC concept was proposed more than a decade ago, but until now has not been implemented in a testbed environment due to a lack of suitable hardware. This thesis presents a proof-of-concept implementation of the meta-MAC protocol by utilizing a programmable radio platform, the Wireless MAC Processor (WMP), in combination with a host-level software module. The implementation of this host module, and the requirements and challenges faced therein, is the primary subject of this thesis. This implementation can combine, with certain constraints, a set of protocols each represented as an extended finite state machine for easy programmability. To illustrate the combination principle, protocols of the same type but with varying parameters are combined in a testbed environment, in what is termed parameter optimization. Specifically, a set of TDMA protocols with differing slot assignments are experimentally combined. This experiment demonstrates that the meta-MAC implementation rapidly converges to non-conflicting TDMA slot assignments for the nodes, with similar results to those in simulation. This both validates that the presented implementation properly implements the meta-MAC protocol, and verifies that the meta-MAC protocol can be as effective on real wireless hardware as it is in simulation.
ContributorsFlick, Nathaniel Graham (Author) / Syrotiuk, Violet (Thesis director) / Fainekos, Georgios (Committee member) / School of Mathematical and Statistical Sciences (Contributor) / Computer Science and Engineering Program (Contributor) / Barrett, The Honors College (Contributor)
Created2016-05
Description
Studies on urban heat island (UHI) have been more than a century after the phenomenon was first discovered in the early 1800s. UHI emerges as the source of many urban environmental problems and exacerbates the living environment in cities. Under the challenges of increasing urbanization and future climate changes, there is a pressing need for sustainable adaptation/mitigation strategies for UHI effects, one popular option being the use of reflective materials. While it is introduced as one effective method to reduce temperature and energy consumption in cities, its impacts on multi-dimensional environmental sustainability and large-scale non-local effect are inadequately explored. This paper provides a synthetic overview of potential environmental impacts of reflective materials at a variety of scales, ranging from energy load on a single building to regional hydroclimate. The review shows that mitigation potential of reflective materials depends on a portfolio of factors, including building characteristics, urban environment, meteorological and geographical conditions, to name a few. Precaution needs to be exercised by city planners and policy makers for large-scale deployment of reflective materials before their environmental impacts, especially on regional hydroclimates, are better understood. In general, it is recommended that optimal strategy for UHI needs to be determined on a city-by-city basis, rather than adopting a “one-solution-fits-all” strategy.
ContributorsYang, Jiachuan (Contributor) / Wang, Zhi-Hua (Correspondent) / Kaloush, Kamil (Contributor)
Created2015-06-11
Description
Waste plastic is considered an environmental pollutant because it is not biodegradable. Therefore, there is increased interest in the use of recycled plastic in pavement construction. Polyethylene terephthalate (PET) is a thermoplastic polymer that is commonly used in the manufacturing of containers and bottles. Waste PET is a durable material that has shown enhancement in performance when introduced into asphalt binder and asphalt mixtures. However, PET particles tend to separate from asphalt because of differences in density, molecular structure, molecular weight, and viscosity, leading to inadequate dispersion of PET particles in the asphalt. This incompatibility between PET and asphalt causes segregation, where storage stability becomes an issue. To solve this problem, applying a surface activation on the PET using another abundant urban waste (waste vegetable oil) was examined in this study, showing this method can be effective to enhance PET-asphalt interactions and consequently the storage stability of PET-modified asphalt. To ensure proper surface activation, it is important to thoroughly understand the chemo-mechanics of asphalt containing PET particles as well as the underlying interaction mechanism at the molecular level. Therefore, this study integrates a multi-scale approach using computational modeling based on density functional theory along with laboratory experiments to provide an in-depth understanding of the mechanisms of interaction between surface-activated PET and asphalt. To do so, the efficacy of bio-oil treatment was examined in terms of both the surface-activation capability and the durability of the resulting PET-modified asphalt. It was found that the grafted bio-oil on the PET particles can make a strong interaction with bituminous composites, leading to enhancing the durability and extending the service life of asphalt pavement by reducing the diffusion of free radicals and moisture into the bulk. The study was further extended to study the effect of coating the PET with biochar, showing the latter coating can improve the mechanical properties of the PET-modified asphalt and the adsorption behavior of the PET for volatile organic compounds. The performance of the waste PET was compared with another widely used modifier, crumb rubber.
ContributorsAldagari, Sand (Author) / Fini, Elham (Thesis advisor) / Kaloush, Kamil (Committee member) / Ozer, Hasan (Committee member) / Arizona State University (Publisher)
Created2024