Modeling and Design of Assured and Adaptive Cyber-Physical Systems
Cyber-Physical Systems (CPS) feature synergetic integration of multiple subsystems to control physical environments through cycles of sensing and actuation. The correct-by-design paradigm aims to provide guarantees on the performance of CPS by utilizing formally-proven algorithms for synthesis and validation of various system components. This paradigm postulates the ability to both derive adequate abstractions of the system, and mathematically formalize design requirements. Therefore, developing mathematical tools that allow system designers to easily model CPS, and to capture design requirements, is imperative to such paradigm.
This dissertation provides theoretical and experimental contributions towards modeling and development of assured and adaptive CPS. In particular, we propose Delayed Action Game (DAG) to aid with modeling CPS where part of the state is hidden from the controller. The formalism deploys the concept of delaying actions as means to hide them from other players without the usage of private variables, allowing the use of off-the-shelf model checkers for analysis. Based on a DAG model, we design an algorithm that utilizes model checkers to synthesize optimal strategies. In addition, we propose Context-Aware Probabilistic Temporal Logic (CAPTL) to aid with formalizing temporal requirements that can naturally described as a set of objectives that are prioritized based on some probabilistic conditions. Furthermore, we develop the algorithm that allow for synthesizing optimal strategies for a Markov Decision Process (MDP) that satisfy a given CAPTL-based requirement.
We deploy the theoretical frameworks in two application domains: human-robot interaction and digital microfluidics, with the goal of designing systems to be more adaptive to their environments. First, we develop protocols for supervisory systems where a human operator, supervising a number of Unmanned Aerial Vehicles (UAVs), can intermittently perform geolocation tasks to aid in detection of possible attacks. We model the system as a DAG, and further use it to synthesize security-aware human-UAV protocols that both provide UAV path plans, increasing the chances of attack detection, and specify the time instances at which the operator is advised to perform a geolocation task. Second, we propose a stochastic game-based framework for droplet routing in Micro-Electrode-Dot Array (MEDA) biochips. The framework utilizes the ability to sense microelectrode health to synthesize routing plans that adapt to the microelectrode degradation levels in run-time. Using multiple real-life bioassays for evaluation, we show that the framework increases the probability of successful completion of benchmark bioassays. Finally, we adapt the framework to utilize Deep Reinforcement Learning (DRL) algorithms to achieve the same task.
This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License.
Rights for Collection: Duke Dissertations
Works are deposited here by their authors, and represent their research and opinions, not that of Duke University. Some materials and descriptions may include offensive content. More info