Matching Items (1,636)
Filtering by
- All Subjects: Electrical Engineering
- All Subjects: literature
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
A new loop configuration capable of reducing power radiation magnitudes lower than conventional loops has been developed. This configuration is demonstrated for the case of two coaxial loops of 0.1 meter radius coupled via the magnetic reactive field. Utilizing electromagnetism theory, techniques from antenna design and a new near field design initiative, the ability to design a magnetic field has been investigated by using a full wave simulation tool. The method for realization is initiated from first order physics model, ADS and onto a full wave situation tool for the case of a non-radiating helical loop. The exploration into the design of a magnetic near field while mitigating radiation power is demonstrated using an real number of twists to form a helical wire loop while biasing the integer twisted loop in a non-conventional moebius termination. The helix loop setup as a moebius loop convention can also be expressed as a shorted antenna scheme. The 0.1 meter radius helix antenna is biased with a 1MHz frequency that categorized the antenna loop as electrically small. It is then demonstrated that helical configuration reduces the electric field and mitigates power radiation into the far field. In order to compare the radiated power reduction performance of the helical loop a shielded loop is used as a baseline for comparison. The shielded loop system of the same geometric size and frequency is shown to have power radiation expressed as -46.1 dBm. The power radiated mitigation method of the helix loop reduces the power radiated from the two loop system down to -98.72 dBm.
ContributorsMoreno, Fernando (Author) / Diaz, Rodolfo (Thesis advisor) / Aberle, James T., 1961- (Committee member) / Kozicki, Michael (Committee member) / Arizona State University (Publisher)
Created2015
Description
In my thesis paper, I examine the gothic elements found in classical gothic fairy tales from European and Japanese tradition, particularly those works by the Brothers Grimm and Yei Theodora Ozaki. By examining the principle gothic elements that are unique to both stories, and further analyzing the commonalities of story, plot, and other major tropes, a better understanding of the message meant to be imparted and other cultural nuances can be ascertained. Gothic literature creates an atmosphere of gloom and suspense, toying with concepts of dread and darkness by employing Gothic elements such as shadows, the supernatural, sinister buildings, and strong-willed villains, all of which affect the rational mind in an irrational way. Fairytales freely use such tropes to their advantage, playing with the many fears of children, while simultaneously painting an idealistic fantasy world. The degree of usage and the application of gothic elements is closely examined in the Grimm works, "Hansel and Gretel," and "The Robber Bridegroom," as well as the Japanese tales, "The Goblin of Adachigahra,""Kintaro the Golden Boy" and "The Monkey and the Crab." These stories have been chosen due for their usage of animal tricksters, themes of control, and aspects of isolation, supernatural entities, and substantial gothic imagery. The gothic elements of death, sinister older women, the supernatural, fears of abandonment, and cunning animals are akin to both Western and Eastern tales, while the concept of gothic setting and the type of monsters prepared to feast on men is significantly different for both cultures, similar lessons are intended to be gleaned by children from these tales, with the intention of generally producing positive results \u2014 while the means differ, the message is strikingly similar, yet there remain cultural differences in terms of central themes and character traits.The effect of re-introducing the darker, gothic elements of traditional fairy tales into modern literature and retellings of the original narratives has been profound.Today, whether it has been at the bequest of the public or simply a new-age movement by modern cinema audience for the "gritty and realistic," fairy tales are returning to their former gothic forms. "Snow White and The Huntsman" is one example of a film which has gone this route, opting for a more gothic, classic telling rather than the chip, cheery, rosy cheeked Disney versions. There is a tendency for most media nowadays to be far less censored and fantastical, aiming for a more realistic, grittier approach \u2014 this bleeds into film and literature likewise, and thus children are impacted by this shift as well. Children seem to be able to handle more, perhaps desensitized at younger and younger ages by the products of our widely consumerist society, or perhaps due to parents raising their children in such a way so that the darkness that tinges these tales doesn't disturb and derail but rather, emphasizes their meaning of teaching certain lessons. Tales such as these are still valuable, and will continue to be so long as we seek a reality greater than our own, where the evil of the world is wiped away, and we all live happily ever after.
ContributorsMoschonas, Jerasimos Theodore (Author) / Ellis, Lawrence (Thesis director) / Hoyt, Heather (Committee member) / Barrett, The Honors College (Contributor) / Department of English (Contributor)
Created2015-05
Description
While SPICE circuit simulation software gives researchers and industry accurate information regarding the behavior and characteristics of circuits, the auditory effect of SPICE circuit simulation on audio circuits is not well documented. This project takes a thoroughly analyzed and popular audio effect circuit called the Ibanez Tubescreamer and simulates its distortion effect on a .wav file in order to hear the effect of SPICE simulation. Specifically, the TS-808 schematic is drawn in the SPICE program LTSPICE and simulated using generated sinusoids and recorded .wav files. Specific components are imported using .MODEL and .SUBCKT to accurately represent the diodes, bipolar transistors, op amps, and other components in order to hear how each component affects the response. Various transient responses are extracted as .wav files and assembled as figures in order to characterize the result of the circuit on the input. Once the actual circuit is built and debugged, all of the same transient analysis is applied and then compared to the SPICE simulation figures gathered in the digital simulation. These results are then compared along with a subjective hearing test of the digital simulation and analog circuit in order to test the validity of the SPICE simulations. The digital simulations reveal that the distortion follows the signature characteristics of Ibanez Tubescreamer which shows that SPICE simulation will give insight into the real effects of audio circuits modeled in SPICE programs. Diodes--such as Silicon, Germanium, Zener, Red LEDs and Blue LEDs--can dramatically change the waveforms and sound of the inputs within the circuit where as the Op-amps--such as the JRC4558, TL072, and NE5532--have little to no effect on the waveforms and subjective effects on the output .wav files. After building the circuit and hearing the difference between the analog circuit and digital simulation, the differences between the two are apparent but very similar in nature--proving that the SPICE simulation can give meaningful insight into the sound of the actual analog circuit. Some of the differences can be explained by the variance of equipment and environment used in recording and playback. Since this project did not use high fidelity audio recording equipment and consistency in the equipment used for playback, it is uncertain if the simulation and actual circuit could be classified as completely accurate. Any further work on the project would be recording and playing back in a constant environment and looking into a wider range of specific components instead of looking into one permutation.
ContributorsMacias, Cole Thomas (Author) / Goryll, Michael (Thesis director) / Yu, Shimeng (Committee member) / Electrical Engineering Program (Contributor) / Barrett, The Honors College (Contributor)
Created2015-12
Description
This thesis explores how the characterization of mentally ill characters evolves in literature within the United States in order to understand if and how modern notions of mental illness have impacted American writers’ fictional depictions of insanity. For this reason, this project compares and contrasts American fiction from the 19th century and 21st century. More specifically, the thesis explores the two centuries to trace evolutions in the use of gothic tropes, the progression of the theme of identity, relevant paratexts, and public conversations about fictional mental illness in modern texts—all of which send specific messages about mental health and impact the ways in which the reader understands the characters with mental illness. Ultimately, this thesis argues that the evolved use of tropes, the theme of identity, paratexts, and public conversations suggest there has been a shift from othering characters with mental illness towards accepting these characters and normalizing mental illness as an ordinary and familiar part of the human experience. In short, an increased understanding of mental health accompanies literary choices that create a more sympathetic representation of mental illness overall, even when fiction writers might still rely heavily on 19th-century tropes regarding madness.
ContributorsHagerman, Rachel L (Author) / Soares, Rebecca (Thesis director) / Murphy, Patricia C. (Committee member) / Department of English (Contributor) / Barrett, The Honors College (Contributor)
Created2020-12
Description
The impact of musical theatre in the United States calls attention to its role in our cultural heritage. Art in all its forms has always been considered to be something of an ongoing history of a society's culture. Musical theatre has been very successful in synthesizing several different aspects of American culture and establishing historical markers in areas of music, drama, social issues, and even technology. The plethora of issues challenged by pieces of music theatre has created a large canon of works that contribute greatly to our culture, both artistically and socially. These works are the result of many centuries of artistic performance and the evolution that these works have gone through over time. Tracing back through vaudeville, Follies, and into the works of European opera: musical theatre has a rich and extensive background in production styles that still inform its presentation today. These styles allow for a dynamic presentation of the ideas and issues that music theatre wishes to address and challenge. When the production style and content of musical works are drawn from these past sources, the oral traditions and storytelling aspects of these works gain renewed prominence. Music theatre as a new frontier of literary study warrants further investigation into its literary merit.
ContributorsMcNay, Michael (Author) / Dreyfoos, Dale (Thesis director) / Harper, Robert (Committee member) / Yatso, Toby (Committee member) / Barrett, The Honors College (Contributor) / College of Liberal Arts and Sciences (Contributor)
Created2012-12