REAFFIRM:基于模型的混合系统修复以提升弹性
系统与控制
2019-02-13 v1
摘要
基于模型的设计为以系统化方式辅助开发者构建可靠且安全的信息物理系统(CPS)提供了一种有前景的途径。在该方法中,设计者首先构建所设计系统的具有数学精确语义的模型,并在从模型生成实现之前针对正确性需求进行广泛分析。然而,随着新漏洞被发现,旨在确保弹性的需求不断演化。目前缺乏一种廉价、自动化的机制来有效修复初始设计,基于模型的系统开发者通常需要从头重新设计与重新实现系统。本文提出一种新方法及名为 REAFFIRM 的 Matlab 工具包,以促进基于模型的修复,提升 CPS 的弹性。REAFFIRM 接收以下输入:1) 建模为 Simulink/Stateflow 图的原始混合系统,2) 给定以模型转换脚本指定的弹性模式,3) 以信号时序逻辑公式表达的安全需求,然后输出满足该需求的修复后模型。REAFFIRM 的整体结构包含两个主要模块:一个模型转换,以及一个构建在伪造工具 Breach 之上的模型综合器。我们引入一种用于混合系统的新模型转换语言,称为 HATL,以允许设计者指定弹性模式。为评估所提方法,我们使用 REAFFIRM 针对 GPS 传感器欺骗攻击下的自适应巡航控制(ACC)系统、滑动模式切换攻击下的单机无限母线(SMIB)系统,以及陀螺仪传感器攻击下的导弹制导系统,自动综合修复模型。
引用
@article{arxiv.1902.04064,
title = {REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency},
author = {Luan Viet Nguyen and Gautam Mohan and James Weimer and Oleg Sokolsky and Insup Lee and Rajeev Alur},
journal= {arXiv preprint arXiv:1902.04064},
year = {2019}
}