CRII: CPS: FAICYS: Model-Based Verification for AI-Enabled Cyber-Physical Systems Through Guided Falsification of Temporal Logic Properties

在智能系统的世界中，数字技术与物理世界发生了迷人的实时融合。这种协同作用通过人工智能（AI）的整合而发生了重大转变，这一举措在极大地增强系统功能的同时，也引入了一层复杂性，在确保其安全性，可靠性和准确性方面提出了新的挑战。不幸的是，在这些先进系统的分析和理解方面存在着巨大的差距，许多最先进的技术无法验证其正确性，特别是与传统系统中的有效性相比。该项目解决了使用集成AI组件测试网络物理系统（CPS）的挑战，使用一种通过模拟找到反例的方法。它解决了分析智能系统中人工智能算法当前采用的关键科学需求。这项研究有可能开发一个开源的证伪工具，伴随着一个数据集包，鼓励在基于模型的验证领域进行更多的创新。在成功完成该项目后，许多工具可以适用于包括AI驱动系统在内的各种其他应用程序。在这个项目中，PI还旨在通过与学术和工业合作伙伴促进集体倡议来弥合现有差距。该项目通过创建有关智能系统和人工智能软件验证的新的基于项目的课程来扩展学习体验。它通过指导本科生和研究生解决现实世界的软件验证问题，进一步丰富了学习，并鼓励更多的女学生参与研究活动。基于最近的研究和初步结果，该项目突出了在基准测试和深入分析AI启用CPS方面的重大差距。它还解决了需要提高检测能力的国家的最先进的技术，专门为这些系统。在第一阶段，该项目通过CPS模型的基准测试和分类，以及对现有伪造方法的大规模实证评估，调查当前采用的支持AI的CPS及其验证实践。该实证研究旨在确定将现有证伪方法应用于AI驱动的CPS模型的局限性和挑战。该研究还探讨了各种模型组件和证伪技术的有效性之间的潜在相关性。这一阶段的见解将使CPS从业者更深入地了解现有软件验证实践中的固有局限性。在第二阶段，该项目开发和评估了一种结合深度强化学习和随机优化的创新方法。这种方法旨在识别输入域中导致系统属性违规的高风险区域，并在这些区域内应用有效的决策。优化过程用于识别最容易违反系统属性的输入区域。识别的高风险区域被集成到强化学习算法的决策策略中，该算法试图定位违反指定属性的最关键的伪造痕迹。这种方法的目标是减少隔离高风险输入区域所需的执行次数，从而增加检测最关键违规的可能性。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

In the world of smart systems, a captivating real-time fusion occurs where digital technology meets the physical world. This synergy has been significantly transformed by the integration of artificial intelligence (AI), a move that, while dramatically enhancing system capabilities, also introduces a layer of complexity, presenting new challenges in ensuring their safety, reliability, and accuracy. Unfortunately, there is a significant gap in the analysis and comprehension of these advanced systems, and many state-of-the-art techniques fall short of verifying their correctness, especially compared to their effectiveness in traditional systems. This project addresses the challenges of testing Cyber Physical Systems (CPS) with integrated AI components, using an approach to find counterexamples by means of simulation. It addresses critical scientific needs for analyzing the current adoptions of AI algorithms within smart systems. This research has the potential to develop an open-source falsification tool, accompanied by a dataset package, encouraging more innovations in the field of model-based verification. Upon successful completion of this project, many of the tools can potentially be adapted to various other applications that include AI-driven systems. In this project, PIs also aim to bridge existing gaps by fostering collective initiatives with academic and industrial partners. The project expands the learning experience by creating new project-based courses on software verification for smart systems and AI. It further enriches learning through mentoring undergraduate and graduate students to solve real-world software verification problems and encourages the involvement of more female students in research activities.Building upon recent research and preliminary results, the project highlights significant gaps in benchmarking and in-depth analysis of AI-enabled CPS. It also addresses the need to improve the detection capabilities of state-of-the-art techniques specifically for these systems. In its first phase, the project investigates current adoptions of AI-enabled CPS and their verification practices through benchmarking and categorization of CPS models, as well as a large-scale empirical assessment of existing falsification methods. The empirical study aims to identify the limitations and challenges of applying existing falsification methods to AI-driven CPS models. The study also explores potential correlations between various model components and the effectiveness of falsification techniques. The insights from this phase will provide CPS practitioners with a deeper understanding of the inherent limitations in existing software verification practices. In its second phase, the project develops and evaluates an innovative approach that combines Deep Reinforcement Learning and Stochastic Optimization. This approach is designed to identify high-risk areas in the input domain leading to system property violations and apply effective decision-making within these regions. The optimization process serves to identify the input areas most prone to violate the system properties. The identified high-risk regions are integrated into the decision-making policy of the reinforcement learning algorithm, which attempts to locate the most critical falsifying traces that violate the specified property. The goal of this approach is to reduce the number of executions required for isolating high-risk input regions, thereby increasing the likelihood of detecting the most critical violations. This endeavor will improve the safety and reliability of AI-driven systems across various real-world applications.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.