CAREER: Formal Methods for Human-Cyber-Physical Systems

University Of Virginia Main Campus, Charlottesville VA

Investigators

Abstract

There is a growing trend toward human-cyber-physical systems (h-CPS), where systems collaborate or interact with human operators to harness complementary strengths of humans and autonomy. Examples include self-driving cars that need the occasional driver intervention, and industrial robots that work beside or cooperatively with people. The societal impact of h-CPS, however, is contingent on ensuring safety and reliability. Several high-profile incidents have shown that unsafe h-CPS can lead to catastrophic outcomes. Formal methods enable the model-based design of safety-critical systems with mathematically rigorous guarantees. However, the research area of formal methods for h-CPS is still in its infancy. The goal of this research is to expand formal methods toward the joint modeling and formal analysis of CPS and human-autonomy interactions, accounting for the uncertainty and variability of human behaviors, intentions, and preferences. The key innovations include new methods to build probabilistic models that can represent unobservable human cognitive states estimated from multi-modal sensing data, and to learn probabilistic specifications for h-CPS; as well as novel probabilistic verification and synthesis techniques to provide correctness guarantees for h-CPS and explainable results that help humans understand counterexamples and synthesized control strategies. If successful, this research will enable the rigorous model-based design of h-CPS such as self-driving cars, thereby contributing to improving safety and cutting development costs. The research outcomes of this project will be integrated into education activities in every phase from graduate courses, to undergraduate capstone research, to outreach efforts for women, underrepresented minorities, and K-12 students. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.