Toward operational safety verification via hybrid automata mining using I/O Traces of AI-Enabled CPS

AI enabled cyber-physical systems such as artificial pancreas suffer from the "no oracle problem". The system is subjected to inputs and scenarios which are not observed during training time and hence the expected outputs are not known. Hence, popular model-based verification techniques that characterize behavior of a control system before deployment using predictive models may be inaccurate and may result in incorrect safety analysis results. In this research, we propose an operational safety verification technique through hybrid system mining from input/output traces of deployed AI-enabled cyber-physical systems. The hybrid automaton model enables formal verification of safety despite the "no oracle problem". We apply our technique to the artificial pancreas control system utilizing data from an outpatient study on an artificial pancreas system.We demonstrate that our technique successfully infers accurate hybrid automata representation of these systems in the field and can be used to perform safety analysis to ascertain safety of the system in presence of inputs and scenarios for which the expected output of the system is unknown. We identify an evaluation scenario under which there exists a clear safety violation.