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

CRII：CPS：FAICYS：通过时态逻辑属性的引导伪造，对支持人工智能的网络物理系统进行基于模型的验证

• 批准号: 2347294
• 负责人: khouloud Gaaloul
• 金额: $ 17.5万
• 依托单位: Regents of the University of Michigan - Dearborn
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-03-01 至 2026-02-28
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2347294&HistoricalAwards=false
• 关键词: CRII; CPS; FAICYS; Model; Based

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.

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