Electrical and Computer Engineering ETDs

Publication Date

Fall 11-15-2019

Abstract

Stochastic reachability is an important verification tool that provides probabilistic assurances of safety in a variety of contexts. In engineered systems, safety may be synonymous with the ability of the system to avoid "bad" constraints on the state space, that constitute collision, departure from a flight envelope, or other undesirable phenomenon. In biomedical systems, assurance of safety (such as the mandate to ``do no harm'') are considerably complicated by the fact that there is a lack of physics-driven models, extensive signal processing is needed to capture the underlying state of the system, and the stochasticity inherent to the system may be quite large. However, assurances of safety are no less paramount. Stochastic reachability analysis is a framework that is well suited to address safety problems in biomedical systems. We are particularly motivated by the problem of circadian regulation, which is not only critical for those with diagnosed sleep disorders, e.g. Delayed Sleep-Wake Phase disorder, but also for shift workers, people traveling across multiple time zones, and those in regulated lighting environments that do not account for circadian regulation, e.g. hospitals. The primary focus of this thesis is on the development software systems and algorithms that can address some of the most significant challenges associated with safety guarantees in biomedical systems. Specifically, I focus on linear time-varying dynamical systems (which are a common approximation of nonlinear dynamical systems) with unstructured, non-Gaussian disturbances. The theoretical methods I develop provide conservative assurances of safety, despite a potentially unbounded disturbance input, in a computable manner. I have implemented these methods in a new MATLAB toolbox for stochastic reachability, SReachTools, that I have jointly developed. This toolbox is open-source and has been repeatability verified. Implementation of such methods in a clinical environment requires rigorous development, design, and testing of software, as well as integration with methods for signal processing, fault handling, and error reporting. As part of a collaboration on smart lighting, I created a software implementation of a smart lighting testbed, which provides the necessary functionality to implement feedback-based circadian control, such as those provided by stochastic reachability algorithms. The testbed software was validated in a pilot experiment, in which the testbed successfully ran continuously for 5 days for each of 3 subjects. Estimates of circadian phase are necessary for control, hence signal processing techniques to infer phase from circadian-regulated biometrics are important. We developed a method to infer circadian phase from invasively gathered brain temperature data, in collaboration with UNM neurosurgeons in the UNM Neurotrauma intensive care unit. A similar technique would be necessary to someday fully close the loop in the smart lighting clinical testbed.

Keywords

Reachability, Software Design, Circadian Rhythms, Control Systems

Document Type

Dissertation

Language

English

Degree Name

Electrical Engineering

Level of Degree

Doctoral

Department Name

Electrical and Computer Engineering

First Committee Member (Chair)

Meeko Oishi

Second Committee Member

R. Scott Erwin

Third Committee Member

Rafael Fierro

Fourth Committee Member

Francesco Sorrentino

Download

Share

COinS