CAREER: Formal Methods for Human-Cyber-Physical Systems

人类-网络-物理系统（h-CPS）的发展趋势越来越明显，在这种系统中，系统与人类操作员协作或交互，以利用人类和自主性的互补优势。例子包括偶尔需要驾驶员干预的自动驾驶汽车，以及在人旁边工作或与人合作的工业机器人。然而，h-CPS的社会影响取决于确保安全性和可靠性。几起备受瞩目的事件表明，不安全的h-CPS可能导致灾难性的后果。形式化方法使安全关键系统的基于模型的设计具有严格的数学保证。然而，h-CPS的形式化方法的研究领域仍处于起步阶段。本研究的目标是扩展形式化方法，对CPS和人类自主互动的联合建模和形式化分析，考虑人类行为，意图和偏好的不确定性和可变性。关键的创新包括建立概率模型的新方法，这些模型可以代表从多模态传感数据估计的不可观察的人类认知状态，并学习h-CPS的概率规范;以及新的概率验证和合成技术，为h-CPS提供正确性保证，并提供可解释的结果，帮助人类理解反例和合成控制策略。如果成功，这项研究将使严格的基于模型的h-CPS设计成为可能，例如自动驾驶汽车，从而有助于提高安全性和降低开发成本。该项目的研究成果将被整合到教育活动的各个阶段，从研究生课程，到本科生的顶点研究，再到针对女性，代表性不足的少数民族和K-12学生的外展工作。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

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.