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）的整合使这种协同作用显着改变了这一举动，尽管这一举动显着增强了系统能力，但也引入了一层复杂性，在确保其安全性，可靠性和准确性方面提出了新的挑战。不幸的是，这些高级系统的分析和理解存在很大的差距，许多最新技术的差异还没有验证其正确性，尤其是与它们在传统系统中的有效性相比。该项目使用一种通过模拟来查找反描述的方法来解决使用集成的AI组件测试网络物理系统（CPS）的挑战。它解决了分析智能系统中AI算法当前采用的关键科学需求。这项研究有可能开发一个开源伪造工具，并附有数据集软件包，鼓励在基于模型的验证领域进行更多创新。成功完成该项目后，许多工具可能会适应包括AI驱动系统在内的其他各种应用程序。在该项目中，PI还旨在通过与学术和工业合作伙伴促进集体计划来弥合现有差距。该项目通过创建有关智能系统和AI软件验证的新课程来扩展学习经验。它通过指导本科和研究生来进一步丰富学习，以解决现实世界中的软件验证问题，并鼓励更多女学生参与研究活动。建立最近的研究和初步结果，该项目突出了对AI-AI-a-Spable CP的基准标准和深入分析的显着差距。它还解决了专门针对这些系统的最新技术的检测能力的需求。在第一阶段，该项目通过基准测试和分类CPS模型研究了当前对AI支持的CP的采用及其验证实践，以及对现有伪造方法的大规模经验评估。实证研究旨在确定将现有伪造方法应用于AI驱动的CPS模型的局限性和挑战。该研究还探讨了各种模型组件与伪造技术的有效性之间的潜在相关性。此阶段的见解将使CPS从业人员对现有软件验证实践的固有局限性有更深入的了解。在第二阶段，该项目开发并评估了一种创新的方法，该方法结合了深度强化学习和随机优化。该方法旨在识别输入域中的高风险区域，导致系统财产违规并在这些地区应用有效的决策。优化过程有助于确定最容易违反系统属性的输入区域。确定的高风险区域被整合到强化学习算法的决策政策中，该算法试图找到违反指定属性的最关键的伪造痕迹。这种方法的目的是减少隔离高风险输入区域所需的执行次数，从而增加检测最严重的违规行为的可能性。这项努力将提高各种现实世界中AI驱动系统的安全性和可靠性。该奖项反映了NSF的法定任务，并认为使用基金会的知识分子优点和更广泛的影响评估标准，认为值得通过评估来获得支持。