Electrical and Computer Engineeringhttp://hdl.handle.net/10012/99082019-08-18T05:11:08Z2019-08-18T05:11:08ZCreating Usage Models to Identify Misbehaving Applications on Mobile DevicesJiang, Qiushihttp://hdl.handle.net/10012/148942019-08-17T02:30:46Z2019-08-16T00:00:00ZCreating Usage Models to Identify Misbehaving Applications on Mobile Devices
Jiang, Qiushi
Limited battery capacity is currently a major pain point for mobile users. The problem
is made worse when poorly designed applications consume a significant amount of power in
the background when they are not actively used by the user. To combat this problem, we
propose an automated monitoring system that can detect misbehaving applications running
on mobile devices. Our system does not require any prior knowledge about the monitored
applications. Instead, it collects the user’s usage records and builds models to encapsulate
the contexts when the user is likely to use each application. From those models, our
system can identify misbehaving applications that are consuming system resources while
providing no useful service to the end user. In this dissertation, we demonstrate the overall
design for our system. This design allows us to collect detailed usage records while keeping
our system’s power consumption at a minimum. We also introduce the steps we take to
construct our usage models and the rationale behind each key decisions. In the end, we
evaluate the effectiveness of our system by running it on a real Android device during a
two month period. From the experiment, we show the misbehaving applications identified
by our system have a significant impact on the battery life, and misbehaving applications
with high network usage is the main cause of fast battery drain.
2019-08-16T00:00:00ZTwo-photon and Three-photon Parametric Interactions in Superconducting Microwave CircuitsChang, Chung Wai Sandbohttp://hdl.handle.net/10012/148922019-08-17T02:30:27Z2019-08-16T00:00:00ZTwo-photon and Three-photon Parametric Interactions in Superconducting Microwave Circuits
Chang, Chung Wai Sandbo
The flexible engineering of superconducting circuits, together with the nonlinearity available from Josephson junctions, have made microwave quantum optics a blooming research field in the past decade. Key experiments originally performed in the optical domain have become very accessible on this microwave-frequency, such that strong atom-field interactions and optical parametric interactions in microwave. From the latter, one example is the implementation of spontaneous parametric downconversion (SPDC). This process is particularly interesting as it can act as a nonclassical radiation source which give a number of potential applications in quantum information processing. We will focus on studying SPDC in microwave throughout this thesis.
In the first half of this thesis, from designs to measurements, we will explore the well-known two-photon parametric processes, SPDC and coherent coupling, which are generated by quadratic Hamiltonians. Using three resonant modes of a SQUID-terminated parametric cavity, we proceeded to combine different two-photon processes in an effort to demonstrate a multipartite nonclassical radiation source. With detailed system gain and noise calibration of our cryogenic microwave network, we confirmed our implementation by experimentally verifying that the generated states contain genuine tripartite entanglement. This multimode entangled radiation source can be an important resource for future experiments on quantum networking.
While two-photon parametric processes have found numerous important applications, they have also been the limit of experiments for over three decades, with higher-order parametric processes seemingly out of reach. In the second half of this thesis, we explore the potential of parametric resonators for achieving such higher-order processes. To do this, we first studied the necessary conditions for accessing cubic Hamiltonians through our SQUID-based interactions. We then fabricated a device dedicated to performing three-photon processes through these cubic Hamiltonians. For the first time, we observed a direct generation of photon triplets by a single SPDC process in microwave . The generation rate can exceed a photon flux density of 60 photon per second per Hertz at the device output, far surpassing any record to date for photon triplets. We studied various pump configurations corresponding to different three-photon SPDC processes starting from a cold vacuum state. Pumping at triple the frequency of a single mode, we observed a phase-space distribution with a non-Gaussian profile which shows strong skewness (third moment) in the quadrature amplitude distribution. We reconstruct the Wigner function of the propagating states from the directly measured moment matrix, demonstrating Wigner negativity. Pumping at the sum frequency of three modes, we observed non-zero coskewness between the quadrature amplitudes of the modes. By analysing the output signals and comparing their characteristics to the predicted theoretical signatures, we confirm our implementation of three-photon SPDC processes generated by specific cubic Hamiltonians. These types of non-Gaussian states have been suggested as a resource enabling universal quantum computation with continuous variables. Our results thus open up the realm of three-photon quantum optics, enabling a wealth of novel experimental and theoretical studies.
2019-08-16T00:00:00ZStrong Induction in Hardware Model CheckingVediramana Krishnan, Hari Govindhttp://hdl.handle.net/10012/148852019-08-15T02:30:47Z2019-08-14T00:00:00ZStrong Induction in Hardware Model Checking
Vediramana Krishnan, Hari Govind
Symbolic Model checking is a widely used technique for automated verification of both hardware and software systems. Unbounded SAT-based Symbolic Model Checking (SMC) algorithms are very popular in hardware verification. The principle of strong induction is one of the first techniques for SMC. While elegant and simple to apply, properties as such can rarely be proven using strong induction and when they can be strengthened, there is no effective strategy to guess the depth of induction. It has been mostly displaced by techniques that compute inductive strengthenings based on interpolation and property directed reachability (PDR). In this thesis, we prove that strong induction is more concise than induction. We then present kAvy, an SMC algorithm that effectively uses strong induction to guide interpolation and PDR-style incremental inductive invariant construction. Unlike pure strong induction, kAvy uses PDR-style generalization to compute and strengthen an inductive trace. Unlike pure PDR, kAvy uses relative strong induction to construct an inductive invariant. The depth of induction is adjusted dynamically by minimizing a proof of unsatisfiability. We have implemented kAvy within the Avy Model Checker and evaluated it on HWMCC instances. Our results show that kAvy is more effective than both Avy and PDR, and that using strong induction leads to faster running time and solving more instances. Further, on a class of benchmarks, called shift, kAvy is orders of magnitude faster than Avy, PDR and pure strong induction.
2019-08-14T00:00:00ZPredictive Runtime Verification of Stochastic SystemsBabaee Cheshmeahmadrezaee, Rezahttp://hdl.handle.net/10012/148762019-08-14T02:30:50Z2019-08-13T00:00:00ZPredictive Runtime Verification of Stochastic Systems
Babaee Cheshmeahmadrezaee, Reza
Runtime Verification (RV) is the formal analysis of the execution of a system against some
properties at runtime. RV is particularly useful for stochastic systems that have a non-zero
probability of failure at runtime. The standard RV assumes constructing a monitor that
checks only the currently observed execution of the system against the given properties.
This dissertation proposes a framework for predictive RV, where the monitor instead
checks the current execution with its finite extensions against some property. The extensions are generated using a prediction model, that is built based on execution samples
randomly generated from the system. The thesis statement is that predictive RV for
stochastic systems is feasible, effective, and useful.
The feasibility is demonstrated by providing a framework, called Prevent, that builds a
predictive monitor by using trained prediction models to finitely extend an execution path,
and computing the probabilities of the extensions that satisfy or violate the given property.
The prediction model is trained using statistical learning techniques from independent and
identically distributed samples of system executions. The prediction is the result of a
quantitative bounded reachability analysis on the product of the prediction model and the
automaton specifying the property. The analysis results are computed offline and stored in
a lookup table. At runtime the monitor obtains the state of the system on the prediction
model based on the observed execution, directly or by approximation, and uses the lookup
table to retrieve the computed probability that the system at the current state will satisfy
or violate the given property within some finite number of steps.
The effectiveness of Prevent is shown by applying abstraction when constructing the
prediction model. The abstraction is on the observation space based on extracting the
symmetry relation between symbols that have similar probabilities to satisfy a property.
The abstraction may introduce nondeterminism in the final model, which is handled by
using a hidden state variable when building the prediction model. We also demonstrate
that, under the convergence conditions of the learning algorithms, the prediction results
from the abstract models are the same as the concrete models.
Finally, the usefulness of Prevent is indicated in real-world applications by showing
how it can be applied for predicting rare properties, properties with very low but non-zero
probability of satisfaction. More specifically, we adjust the training algorithm that uses
the samples generated by importance sampling to generate the prediction models for rare
properties without increasing the number of samples and without having a negative impact
on the prediction accuracy.
2019-08-13T00:00:00Z