Formal Models of Human Control and Interaction with Cyber Physical Systems.pdf

Abstract:

One of the most important challenges in the design and deployment of Cyber-Physical Systems is how to formally guarantee that they are amenable to effective human control. This is a challenging problem not only because of the operational changes and increasing complexity of future CPS but also because of the nonlinear nature of the human-CPS system under realistic assumptions. Current state of the art has in general produced simplified models and has not fully considered realistic assumptions about system and environmental constraints or human cognitive abilities and limitations. To overcome current state of the art limitations, our overall research goal is to develop a theoretical framework for complex human-CPS that enables formal analysis and verification under realistic assumptions about the operation environment, model uncertainties and human cognitive limitations and abilities. In particular, we aim to develop a cognitively plausible analytic model of a human operator, integrate it into a hybrid system model of CPS and verify the integrated human-CPS system. To this end, we designed a control task for a robot swarm in an environment with obstacles. The robotic swarm had different behaviors (e.g. rendezvous, deploy) to cover the environment. Human experimental data was collected where the participants had to decide which behavior to select for each trial. An ACT-R cognitive model was developed that reflected the human performance data. We are currently working towards abstracting a Markov model from the ACT-R model. We have also developed methods to verify classes of discrete-time stochastic hybrid systems via chance constrained information for the perfect information case, and via point-based value iteration for the incomplete information case.