This NSF Cyber-Physical Systems (CPS) Frontier project "Verified Human Interfaces, Control, and Learning for Semi-Autonomous Systems (VeHICaL)" is developing the foundations of verified co-design of interfaces and control for human cyber-physical systems (h-CPS) --- cyber-physical systems that operate in concert with human operators. VeHICaL aims to bring a formal approach to designing both interfaces and control for h-CPS, with provable guarantees. The VeHICaL project is grounded in a novel problem formulation that elucidates the unique requirements on h-CPS including not only traditional correctness properties on autonomous controllers but also quantitative requirements on the logic governing switching or sharing of control between human operator and autonomous controller, the user interface, privacy properties, etc. The project is making contributions along four thrusts: (1) formalisms for modeling h-CPS; (2) computational techniques for learning, verification, and control of h-CPS; (3) design and validation of sensor and human-machine interfaces, and (4) empirical evaluation in the domain of semi-autonomous vehicles. The VeHICaL approach is bringing a conceptual shift of focus away from separately addressing the design of control systems and human-machine interaction and towards the joint co-design of human interfaces and control using common modeling formalisms and requirements on the entire system. This co-design approach is making novel intellectual contributions to the areas of formal methods, control theory, sensing and perception, cognitive science, and human-machine interfaces. Cyber-physical systems deployed in societal-scale applications almost always interact with humans. The foundational work being pursued in the VeHICaL project is being validated in two application domains: semi-autonomous ground vehicles that interact with human drivers, and semi-autonomous aerial vehicles (drones) that interact with human operators. A principled approach to h-CPS design --- one that obtains provable guarantees on system behavior with humans in the loop --- can have an enormous positive impact on the emerging national ``smart'' infrastructure. In addition, this project is pursuing a substantial educational and outreach program including: (i) integrating research into undergraduate and graduate coursework, especially capstone projects; (ii) extensive online course content leveraging existing work by the PIs; (iii) a strong undergraduate research program, and (iv) outreach and summer programs for school children with a focus on reaching under-represented groups.

This NSF Cyber-Physical Systems (CPS) Frontier project "Verified Human Interfaces, Control, and Learning for Semi-Autonomous Systems (VeHICaL)" is developing the foundations of verified co-design of interfaces and control for human cyber-physical systems (h-CPS) --- cyber-physical systems that operate in concert with human operators. VeHICaL aims to bring a formal approach to designing both interfaces and control for h-CPS, with provable guarantees. The VeHICaL project is grounded in a novel problem formulation that elucidates the unique requirements on h-CPS including not only traditional correctness properties on autonomous controllers but also quantitative requirements on the logic governing switching or sharing of control between human operator and autonomous controller, the user interface, privacy properties, etc. The project is making contributions along four thrusts: (1) formalisms for modeling h-CPS; (2) computational techniques for learning, verification, and control of h-CPS; (3) design and validation of sensor and human-machine interfaces, and (4) empirical evaluation in the domain of semi-autonomous vehicles. The VeHICaL approach is bringing a conceptual shift of focus away from separately addressing the design of control systems and human-machine interaction and towards the joint co-design of human interfaces and control using common modeling formalisms and requirements on the entire system. This co-design approach is making novel intellectual contributions to the areas of formal methods, control theory, sensing and perception, cognitive science, and human-machine interfaces. Cyber-physical systems deployed in societal-scale applications almost always interact with humans. The foundational work being pursued in the VeHICaL project is being validated in two application domains: semi-autonomous ground vehicles that interact with human drivers, and semi-autonomous aerial vehicles (drones) that interact with human operators. A principled approach to h-CPS design --- one that obtains provable guarantees on system behavior with humans in the loop --- can have an enormous positive impact on the emerging national ``smart'' infrastructure. In addition, this project is pursuing a substantial educational and outreach program including: (i) integrating research into undergraduate and graduate coursework, especially capstone projects; (ii) extensive online course content leveraging existing work by the PIs; (iii) a strong undergraduate research program, and (iv) outreach and summer programs for school children with a focus on reaching under-represented groups.