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

确保嵌入式控制系统的安全性，例如用于汽车的嵌入式控制系统，是非常困难的，正如近年来许多召回的汽车所显示的，每年造成数百亿美元的经济损失。该项目旨在通过开发安全防护装置来提高嵌入式控制系统中关键部件的安全性，安全防护装置是根据安全要求自动生成并附在原始系统上的反应性部件，以确保即使原始系统违反安全要求，组合系统也是安全的。这个项目的智力价值在于一套方法和工具，以综合黑盒系统的安全警卫。具体而言，该项目包括三个研究任务：（a）建立一个基准套件的关键组件及其安全要求;（B）开发合成算法，用于构建有限状态机（FSM）的安全警卫;和（c）开发软件合成工具，用于自动生成软件代码，实现这些FSM。该研究项目将使广泛的应用领域受益，包括汽车和航空电子设备，这些领域将通过与工业界的合作进行研究。它将有助于提高关键组件的安全性，包括基于机器学习和人工智能技术的组件。它将简化认证，因为相对简单的安全防护装置可以根据安全要求进行认证，而不是关键部件的详细模型。最后但并非最不重要的是，它将简化开发过程，让人们专注于功能和性能，而不必同时担心安全违规。由此产生的软件工具以及评价基准和实验数据将向公众提供。为便于传播和分享，该项目将维持在线文件、教程、幻灯片以及工具和基准储存库的源代码。除了弗吉尼亚理工大学和南加州大学的参与者的研究网站外，以下网站将致力于广泛传播项目成果：http://chaowang-vt.github.io/safetyguard/This奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识价值和更广泛的影响审查标准进行评估来支持。

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.