Collaborative Research: CPS: Medium: Spatio-Temporal Logics for Analyzing and Querying Perception Systems

自动驾驶系统（ADS）和高级驾驶辅助系统（ADAS）的目标包括减少意外死亡，增强残疾人士的机动性，以及全面改善公众的生活质量。这类系统通常在开放和高度不确定的环境中运行，因此强大的感知系统是必不可少的。然而，尽管在计算机视觉、机器学习和传感器融合方面取得了巨大的理论和实验进展，但对感知组件提供保证的形式和条件仍然不清楚。最先进的技术是根据地面真值执行基于场景的数据评估，但这只有有限的影响。缺乏正式的指标来分析感知系统的质量，已经导致了几起灾难性事件，并使ADS/ADAS的发展停滞不前。该项目开发了用于指定和评估ADS和ADAS应用程序中感知子系统的质量和健壮性的正式语言。为了使这项技术得到更广泛的传播，该项目开发了研究生和本科生课程，培训工程师使用这些方法，并开发了新的教育模块，解释为推广和公众参与活动开发安全可靠的ADS所面临的挑战。为了扩大计算机领域的参与，研究人员的目标是通过暑期实习将本科女生纳入研发阶段。在这个项目中开发的形式语言是基于研究者开创的一种新的时空逻辑。这种逻辑允许人们同时对流感知数据进行时间推理，并在数据的单个帧内和跨帧内对对象进行空间推理。该项目还为该逻辑开发了定量语义，为用户提供了感知子系统的可量化质量度量。这些语义支持在不同的感知系统和架构之间进行比较。至关重要的是，形式化语言促进了抽象实现细节的过程，这反过来又允许系统设计者和管理者在更高的抽象层次上为系统性能指定假设和保证。这种形式化语言的一个有趣的好处是，它支持使用特定驾驶场景的感知数据查询数据库，而不需要高度手动创建基础事实注释的过程。这样的正式语言目前还不存在，这是为安全关键系统中使用的感知组件建立繁荣市场的巨大障碍。该框架为感知组件供应商和汽车公司之间的需求语言奠定了基础。在这个项目中开发的开源和公开可用的软件工具将帮助工程师和政府机构测试感知系统。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The goals of Automated Driving Systems (ADS) and Advanced Driver Assistance Systems (ADAS) include reduction in accidental deaths, enhanced mobility for differently abled people, and an overall improvement in the quality of life for the general public. Such systems typically operate in open and highly uncertain environments for which robust perception systems are essential. However, despite the tremendous theoretical and experimental progress in computer vision, machine learning, and sensor fusion, the form and conditions under which guarantees should be provided for perception components is still unclear. The state-of-the-art is to perform scenario-based evaluation of data against ground truth values, but this has only limited impact. The lack of formal metrics to analyze the quality of perception systems has already led to several catastrophic incidents and a plateau in ADS/ADAS development. This project develops formal languages for specifying and evaluating the quality and robustness of perception sub-systems within ADS and ADAS applications. To enable broader dissemination of this technology, the project develops graduate and undergraduate curricula to train engineers in the use of such methods, and new educational modules to explain the challenges in developing safe and robust ADS for outreach and public engagement activities. To broaden participation in computing, the investigators target the inclusion of undergraduate women in research and development phases through summer internships.The formal language developed in this project is based on a new spatio-temporal logic pioneered by the investigators. This logic allows one to simultaneously perform temporal reasoning about streaming perception data, and spatially reason about objects both within a single frame of the data and across frames. The project also develops quantitative semantics for this logic, which provides the user with quantifiable quality metrics for perception sub-systems. These semantics enable comparisons between different perception systems and architectures. Crucially, the formal language facilitates the process of abstracting away implementation details, which in turn allows system designers and regulators to specify assumptions and guarantees for system performance at a higher-level of abstraction. An interesting benefit of this formal language is that it enables querying of databases with perception data for specific driving scenarios without the need for the highly manual process of creating ground truth annotations. Such a formal language currently does not exist, and this is a huge impediment to building a thriving marketplace for perception components used in safety-critical systems. This framework sets the foundation for a requirements language between suppliers of perception components and automotive companies. The open source and publicly available software tools developed in this project will assist with testing of perception systems by engineers and governmental agencies.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.