REAFFIRM: 为提高容错性而改进混合系统的模型修复
REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency
AI总结：
本文提出了一种新的模型修复方法和Matlab工具包REAFFIRM，用于通过模型修复提高车载系统（CPSs）的容错性。该方法通过混合系统模型变换和模型综合工具，基于安全要求生成修复后的模型。
摘要：
基于模型的设计提供了一种有前途的方法，帮助开发者系统性地构建可靠和安全的车载系统（CPSs）。在该方法中，设计师首先构建一个具有数学精确语义的系统模型，并在生成实现之前进行广泛的正确性分析。然而，随着新漏洞的发现，需求不断演变，以确保容错性。目前缺乏一种经济、自动的机制，可以有效地修复初始设计，导致系统开发者经常需要重新设计和重新实现系统。本文提出了一种新的方法和名为REAFFIRM的Matlab工具包，以促进模型修复，提高CPSs的容错性。REAFFIRM的输入包括1）原始混合系统建模为Simulink/Stateflow图，2）给定的容错模式指定为模型转换脚本，3）安全要求表达为信号时间逻辑公式，然后输出满足要求的修复模型。REAFFIRM的整体结构包含两个主要模块，模型转换和基于否定工具Breach构建的模型综合器。我们引入了一种新的混合系统模型转换语言HATL，允许设计师指定容错模式。为了评估所提出的方法，我们使用REAFFIRM自动综合修复模型，用于在GPS传感器欺骗攻击下的自适应巡航控制系统，单机无穷大母线系统（SMIB）下的滑模切换攻击，以及导弹制导系统下的陀螺仪传感器攻击。
英文摘要：
Model-based design offers a promising approach for assisting developers to build reliable and secure cyber-physical systems (CPSs) in a systematic manner. In this methodology, a designer first constructs a model, with mathematically precise semantics, of the system under design, and performs extensive analysis with respect to correctness requirements before generating the implementation from the model. However, as new vulnerabilities are discovered, requirements evolve aimed at ensuring resiliency. There is currently a shortage of an inexpensive, automated mechanism that can effectively repair the initial design, and a model-based system developer regularly needs to redesign and reimplement the system from scratch. In this paper, we propose a new methodology along with a Matlab toolkit called REAFFIRM to facilitate the model-based repair for improving the resiliency of CPSs. REAFFIRM takes the inputs including 1) an original hybrid system modeled as a Simulink/Stateflow diagram, 2) a given resiliency pattern specified as a model transformation script, and 3) a safety requirement expressed as a Signal Temporal Logic formula, and then outputs a repaired model which satisfies the requirement. The overall structure of REAFFIRM contains two main modules, a model transformation, and a model synthesizer built on top of the falsification tool Breach. We introduce a new model transformation language for hybrid systems, which we call HATL to allow a designer to specify resiliency patterns. To evaluate the proposed approach, we use REAFFIRM to automatically synthesize repaired models for an adaptive cruise control (ACC) system under a GPS sensor spoofing attack, for a single-machine infinite-bus (SMIB) system under a sliding-mode switching attack, and for a missile guidance system under gyroscopes sensor attack.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
