CSR: Small: Collaborative Research: Safety Guard: A Formal Approach to Safety Enforcement in Embedded Control Systems

CSR：小型：协作研究：安全卫士：嵌入式控制系统中安全执行的正式方法

• 批准号: 1813117
• 负责人: Chao Wang
• 金额: $ 25万
• 依托单位: University of Southern California
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-08-01 至 2022-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1813117&HistoricalAwards=false
• 关键词: CSR; Small; Collaborative; Research; Safety

Ensuring the safety of embedded control systems, such as the ones used in cars, is remarkably difficult as shown by the many recalled cars in recent years, causing tens of billions of financial loss each year. This project aims to improve the safety of critical components in embedded control systems by developing safety guards, a reactive component generated automatically from safety requirements and attached to the original system, to ensure the combined system is safe even if the original system violates the safety requirements. The intellectual merit of this project lies in the set of methods and tools to be developed for synthesizing safety guards of black-box systems. Specifically, this project consists of three research tasks: (a) building a benchmark suite of critical components and their safety requirements; (b) developing synthesis algorithms for constructing the finite-state machines (FSMs) of the safety guards; and (c) developing software synthesis tools for automatically generating software code that implements these FSMs. This research project will benefit a wide range of application domains, including automotive and avionics, which will be investigated through collaborations with industry. It will help improve the safety of critical components, including those based on machine learning and artificial intelligence techniques. It will simplify certification since the relatively simple safety guard can be certified against safety requirements in place of the detailed model of a critical component. And last but not the least, it will simplify the development process by allowing people to focus on functionality and performance without worrying about safety violations at the same time. The resulting software tools, together with evaluation benchmarks and experimental data, will be made available to the public. To facilitate dissemination and sharing, the project will maintain online documentations, tutorials, slides, and source code of the tool and benchmark repositories. Besides the research websites of participants at Virginia Tech and University of Southern California, the following website will be dedicated to disseminate the project results broadly: http://chaowang-vt.github.io/safetyguard/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.

确保嵌入式控制系统的安全性（例如汽车中使用的系统）非常困难，近年来许多被召回的汽车表明，每年造成数以万计的财务损失。该项目旨在通过开发安全保护罩（由安全要求自动生成并附加到原始系统中，即使原始系统违反了安全要求也是安全的，因此可以自动生成的安全部件来提高嵌入式控制系统中关键组件的安全性。该项目的智力优点在于为了综合黑盒系统的安全后卫而开发的一组方法和工具。具体而言，该项目由三个研究任务组成：（a）建立一组基准的关键组件及其安全要求； （b）开发用于构建安全守卫的有限状态机（FSM）的合成算法； （c）开发用于自动生成实现这些FSM的软件代码的软件合成工具。该研究项目将使包括汽车和航空电子设备在内的广泛应用领域受益，这将通过与行业的合作进行调查。它将有助于提高关键组件的安全性，包括基于机器学习和人工智能技术的组件。它将简化认证，因为可以根据安全要求代替关键组件的详细模型来认证相对简单的安全保护人员。最后但并非最不重要的一点是，它将通过允许人们专注于功能和绩效而不必担心安全违规行为来简化开发过程。最终的软件工具以及评估基准和实验数据将提供给公众。为了促进传播和共享，该项目将维护工具和基准存储库的在线文档，教程，幻灯片和源代码。 Besides the research websites of participants at Virginia Tech and University of Southern California, the following website will be dedicated to disseminate the project results broadly: http://chaowang-vt.github.io/safetyguard/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.

项目成果

Synthesizing Fair Decision Trees via Iterative Constraint Solving

通过迭代约束求解综合公平决策树

• 发表时间: 2022
• 期刊: International Conference on Computer Aided Verification
• 作者: Wang, Jingbo;Li, Yannan;Wang, Chao
• 通讯作者: Wang, Chao

DiffRNN: Differential Verification of Recurrent Neural Networks

• DOI: 10.1007/978-3-030-85037-1_8
• 发表时间: 2020-07
• 作者: Sara Mohammadinejad;Brandon Paulsen;Chao Wang;Jyotirmoy V. Deshmukh

LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions

• DOI: 10.1007/978-3-030-99524-9_19
• 发表时间: 2022-01
• 期刊: ArXiv
• 作者: Brandon Paulsen;Chao Wang

Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems

真实的护盾合成：增强网络物理系统的安全性

• DOI: 10.23919/fmcad.2019.8894264
• 发表时间: 2019
• 期刊: 2019 Formal Methods in Computer Aided Design (FMCAD
• 作者: Wu, Meng;Wang, Jingbo;Deshmukh, Jyotirmoy;Wang, Chao
• 通讯作者: Wang, Chao

Example Guided Synthesis of Linear Approximations for Neural Network Verification

• DOI: 10.1007/978-3-031-13185-1_8
• 发表时间: 2022
• 作者: Brandon Paulsen;Chao Wang