FMitF: Track II: Hybrid and Dynamical Systems Verification on the CPS-VO

FMITF：轨道 II：CPS-VO 上的混合动力系统验证

• 批准号: 1918450
• 负责人: Taylor Johnson
• 金额: $ 9.83万
• 依托单位: Vanderbilt University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2022-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1918450&HistoricalAwards=false
• 关键词: FMitF; Track; II; Hybrid; Dynamical

This project aims to transition recent research results that automate portions of the verification process of Cyber-Physical Systems into broader practice, particularly with industrial and student users. Cyber-physical systems (CPS) are networked embedded computing systems coupled with physics, such as in motor vehicles, aircraft, medical devices, and the electrical grid. Due to their frequent use in safety-critical scenarios where significant losses may be incurred, such as of human life or monetarily, the engineering process for such systems devotes vast resources to the process of verification to ensure these systems meet their requirements. The approach builds upon recent successes in the hybrid systems verification competition (ARCH-COMP) hosted in the past three years, in which several dozen hybrid systems verification tools have competed across several problem and system categories. To achieve the transition of verification research results for CPS models into broader practice, this project develops a cloud-based framework to interface with and execute state-of-the-art formal verification software tools from the hybrid and dynamical systems verification community using NSF's CPS Virtual Organization (CPS-VO). The project extends the Design Studio and Tool Integration frameworks for the CPS-VO, to provide an easy-to-use interface for these verification tools. It also serves as a repository for housing executable versions of the tools and benchmarks, plus facilitating repeatability evaluations for ARCH-COMP through a distributed, cloud-based execution architecture. The core technology upon which the tool is built is the hybrid systems model source transformation and translation (HyST) software tool, which performs semantics-preserving translation between state-of-the-art hybrid systems verification tools.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.

该项目旨在将最近的研究成果转化为更广泛的实践，特别是工业和学生用户，这些成果将网络物理系统验证过程的部分自动化。网络物理系统 (CPS) 是与物理耦合的网络嵌入式计算系统，例如机动车辆、飞机、医疗设备和电网。由于它们经常用于可能造成重大损失（例如人命或金钱）的安全关键场景，因此此类系统的工程流程投入了大量资源进行验证过程，以确保这些系统满足其要求。该方法建立在过去三年举办的混合系统验证竞赛 (ARCH-COMP) 的成功基础上，其中有数十种混合系统验证工具针对多个问题和系统类别进行了竞争。为了将 CPS 模型的验证研究成果转化为更广泛的实践，该项目开发了一个基于云的框架，使用 NSF 的 CPS 与混合动力系统验证社区的最先进的形式验证软件工具进行交互并执行虚拟组织（CPS-VO）。该项目扩展了 CPS-VO 的设计工作室和工具集成框架，为这些验证工具提供易于使用的界面。它还充当存储工具和基准的可执行版本的存储库，并通过分布式、基于云的执行架构促进 ARCH-COMP 的可重复性评估。该工具构建的核心技术是混合系统模型源转换和翻译 (HyST) 软件工具，该工具在最先进的混合系统验证工具之间执行语义保留的翻译。该奖项反映了 NSF 的法定使命和通过使用基金会的智力优点和更广泛的影响审查标准进行评估，该项目被认为值得支持。

项目成果

Evaluation of Neural Network Verification Methods for Air-to-Air Collision Avoidance

• DOI: 10.2514/1.d0255
• 发表时间: 2022-10
• 期刊: Journal of Air Transportation
• 作者: Diego Manzanas Lopez;Taylor T. Johnson;Stanley Bak;Hoang-Dung Tran;Kerianne L. Hobbs

A Framework for Identification and Validation of Affine Hybrid Automata from Input-Output Traces

从输入输出轨迹识别和验证仿射混合自动机的框架

• DOI: 10.1145/3470455
• 发表时间: 2022
• 期刊: ACM Transactions on cyber-physical systems
• 影响因子: 2.3
• 作者: Xiaodong Yang, Omar Ali

Verification of Neural Network Compression of ACAS Xu Lookup Tables with Star Set Reachability

ACAS Xu查找表神经网络压缩星集可达性验证

• DOI: 10.2514/6.2021-0995
• 发表时间: 2021
• 期刊: AIAA Scitech 2021 Forum
• 作者: Manzanas Lopez, Diego;Johnson, Taylor;Tran, Hoang-Dung;Bak, Stanley;Chen, Xin;Hobbs, Kerianne L.
• 通讯作者: Hobbs, Kerianne L.

Partial Differential Equation Driven Dynamic Graph Networks for Predicting Stream Water Temperature

• DOI: 10.1109/icdm51629.2021.00011
• 发表时间: 2021-01-01
• 期刊: 2021 21ST IEEE INTERNATIONAL CONFERENCE ON DATA MINING (ICDM 2021)
• 作者: Bao, Tianshu;Jia, Xiaowei;Johnson, Taylor T.
• 通讯作者: Johnson, Taylor T.

ARCH-COMP21 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants

• DOI: 10.29007/kfk9
• 发表时间: 2021
• 作者: Taylor T. Johnson;Diego Manzanas Lopez;Luis Benet;M. Forets;Sebastián Guadalupe;Christian Schilling;Radoslav Ivanov;Taylor J. Carpenter;James Weimer;Insup Lee