Statistically Sound Verification and Optimization of Black-Box Systems

Zhang, Yan

Graduate Thesis Or Dissertation

Statistically Sound Verification and Optimization of Black-Box Systems Public Deposited

Analytics

Citations

Citeable URL: https://scholar.colorado.edu/concern/graduate_thesis_or_dissertations/q524jp19f

Abstract

This thesis discusses two important problems for the design of practical systems under stochastic parameter variations: verification and optimization. Verification is concerned with the safety of a system, i.e., whether a system satisfies its specifications. If not, optimization is applied to tune the design parameters in the system so that the new design is safe. This thesis treats systems as black-boxes, assuming that the systems can be simulated efficiently but without detailed knowledge of the internal workings. It presents a series of simulation-based techniques to solve the problems of design verification and optimization. A notion called statistical soundness is introduced in this thesis, which guarantees that the outcome of the proposed techniques are “statistically certified” in the sense that the probability of drawing a wrong conclusion is bounded. For the problem of verification, this thesis develops a statistically sound model inference (SSMI) approach. SSMI constructs statistically sound models to explain the relationship between the stochastic parameters and the responses of a system. To improve the scalability of SSMI, a sparse approximation algorithm is also introduced. For the problem of optimization, this thesis presents a statistically sound optimization technique, SSMI-opt. SSMI-opt aims to find values of the design parameters for which the system satisfies the specifications. The proposed techniques can be applied to many interesting areas, including analog/mixd-signal circuits, embedded systems, biological systems, and medical devices. This thesis demonstrates the utility of this methodology on several interesting benchmark examples.

Creator