Conformance Testing as Falsification for Cyber-Physical Systems
Arizona State University(亚利桑那州立大学);Toyota Technical Center(丰田技术中心)
本文提出将符合性定义为系统间的距离度量,设计了检测非符合性的算法并测量符合程度,通过多个模型验证了方法的有效性。
2014-05-31 cs.SY eess.SY
Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches
混杂系统的证伪作为穷举形式化验证的一种实用替代方法,在信息物理系统(CPS)的质量保证中引起了越来越多的关注。在证伪中,人们寻找一个证伪输入,它驱动一个给定的黑盒模型输出一个不希望的信号。在本文中,我们确定输入约束-如约束“油门和刹车踏板不应同时按下”的汽车动力系统模型-作为一个关键因素的证伪方法的实用价值。我们提出了三种方法,系统地解决输入约束优化为基础的证伪,其中两个来自字典法的约束多目标优化的背景下研究。实验证明了该方法的有效性。
2020-04-13 cs.SY eess.SY
Large Language Models as Falsifiers for Cyber-Physical Systems
Stony Brook University(石溪大学)
本文提出LLM-Falsifier,利用大型语言模型最小化STL鲁棒性,通过引入语义信息实现更高效的CPS规范反例搜索,在ARCH-COMP基准上超越现有工具。
2026-09-18 cs.AI cs.LO cs.SE
Constrained Optimization for Hybrid System Falsification and Application to Conjunctive Synthesis
信息物理系统(CPS)的综合问题是寻找一个输入信号,使系统的行为满足给定的规范。我们的设定是,规范是信号时序逻辑的公式,而且,规范是不同的,往往是相互冲突的要求的结合。合取规范对于基于优化的证伪(CPS分析的一种已建立的方法,也可用于合成)通常具有挑战性,因为通常的框架(特别是其强大的语义如何处理布尔连接词)不适合在不同需求之间找到微妙的权衡。我们所提出的方法包括基于优化的证伪和约束优化的组合。具体来说,我们表明,国家的最先进的多约束排名方法可以与伪造的CMA-ES优化供电相结合,其性能优势在实验中得到证明。
2021-02-10 cs.SY eess.SY
RampoNN: A Reachability-Guided System Falsification for Efficient Cyber-Kinetic Vulnerability Detection
University of California, Irvine(加州大学尔湾分校)
本文提出RampoNN框架,通过控制代码、物理系统模型和信号时间逻辑规范,系统识别网络-物理漏洞。利用深度伯恩斯坦神经网络提高可达性分析精度,加速漏洞检测并提升可扩展性。
2026-04-01 cs.CR cs.SY eess.SY
Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans
网络物理系统(CPS)是具有物理和软件组件的系统,例如汽车和工业机器人。由于这些系统表现出离散和连续的动态,它们是复杂的,因此很难验证它们的行为是否符合预期。时序逻辑性质的证伪是通过模拟来寻找CPS反例的一种方法。在本文中,我们提出了两个补充,以提高伪造的能力,使其在大规模的工业环境中更可行。第一个增加的是一个框架,用于将规范从基于信号的模型转换为信号时序逻辑。第二个补充是在证伪过程中使用值布尔和添加剂鲁棒语义。我们评估了一组基准模型上的附加鲁棒语义的性能,我们可以看到,哪些语义是更可取的依赖于模型和规范。
2019-10-18 cs.SY eess.SY
Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification (Extended Version)
National Institute of Informatics(国立情报学研究所);SOKENDAI (The Graduate University for Advanced Studies)(综合研究大学院大学)
本文针对混合系统反驳中布尔连结词的尺度问题,提出一种结合多臂老虎机算法的改进方法,通过引入新的奖励概念'爬升收益'来提升鲁棒性,并在实验中证明其优于现有工具。
2019-06-23 cs.SY eess.SY
Active Requirement Mining of Bounded-Time Temporal Properties of Cyber-Physical Systems
本文通过主动学习方法解决网络物理系统bounded-time信号时间要求挖掘问题,提出GP-ACB算法提升 falsification问题求解效率,实验表明其在Ackley函数和自动变速器模型中优于Nelder-Mead算法,平均提升30%-40%。
2016-03-02 cs.SY eess.SY
PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems
在本文中,我们提出了Python包PSY-TaLiRo,这是一个工具箱的时间逻辑鲁棒性引导证伪的网络物理系统(CPS)。PSY-TaLiRo是一个完全模块化的工具箱,支持多个时序逻辑离线监视器以及用于测试用例生成的优化引擎。PSY-TaLiRo的好处之一是,它支持许多不同类型的被测系统的基于搜索的测试生成。所有的PSY-TaLiRo模块都可以由用户完全修改,以支持新的优化和鲁棒性计算引擎以及任何被测系统(SUT)。
2021-06-04 cs.SE cs.SY eess.SY
Investigating Robustness in Cyber-Physical Systems: Specification-Centric Analysis in the face of System Deviations
本文针对信息物理系统(CPS)在环境干扰下的鲁棒性问题,提出基于规约的鲁棒性定义及证伪问题,并构建双层仿真分析框架,通过基准测试有效识别鲁棒性违规,为比较传统与强化学习控制器提供了见解。
2024-03-25 cs.LO cs.SE cs.SY
Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Carnegie Mellon University(卡内基梅隆大学);The Pennsylvania State University(宾夕法尼亚州立大学);Toyota InfoTech Labs(丰田信息技术实验室)
本文针对信息物理系统中强化学习控制器的容忍度问题,提出了基于信号时序逻辑的容忍度证伪问题,并设计了双层仿真分析框架与搜索启发式方法,有效发现导致系统违规的微小偏差。
2024-06-24 cs.AI cs.LO cs.RO
Coverage Explorer: Coverage-guided Test Generation for Cyber Physical Systems
针对CPS测试覆盖率不足的问题,提出Coverage Explorer框架,结合覆盖率采样、聚类代理模型与模型预测控制生成测试用例,在多个基准上验证了其有效性。
2023-12-04 cs.NA cs.SY eess.SY
A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems
Stanford University(斯坦福大学);NASA Ames Research Center(美国国家航空航天局埃姆斯研究中心)
自主网络物理系统(CPS)可以提高安全关键型应用的安全性和效率,但在部署前需要进行严格的测试。这些系统的复杂性通常排除了形式化验证的使用,并且在开发期间,真实世界的测试可能太危险。因此,已经开发了基于仿真的技术,将被测系统视为在仿真环境中运行的黑盒。安全验证任务包括发现环境中导致系统故障(伪造)的干扰,发现最可能的故障,并估计系统故障的概率。出于安全关键的人工智能的流行,这项工作提供了一个国家的最先进的CPS安全验证技术的调查,重点是应用算法和修改的安全验证问题。我们提出并讨论了优化,路径规划,强化学习和重要性采样领域的算法。问题分解技术,以帮助规模的算法,以大的状态空间,这是常见的CPS。简要概述了安全关键应用,包括自动驾驶汽车和飞机防撞系统。最后,我们提出了现有的学术和商业上可用的安全验证工具的调查。
2021-10-14 cs.AI cs.LG cs.SY
Optimal deception attack on networked vehicular cyber physical systems
在这里,设计的虚假数据注入攻击的分布式网络物理系统。一个具有线性动力学和高斯噪声的随机过程由多个代理节点测量,每个代理节点配备多个传感器。代理节点在它们之间形成多跳网络。每个代理节点通过使用其传感器观测和从相邻节点获得的消息,通过卡尔曼共识滤波来计算过程的估计。外部攻击者能够任意操纵部分或全部代理节点的传感器观测值,将错误注入这些传感器观测值。攻击者的目标是引导代理节点处的估计尽可能接近预先指定的值,同时尊重对攻击检测概率的约束。为此,一个约束优化问题,制定了某种类型的线性攻击的最佳参数值。通过随机逼近和在线随机梯度下降相结合的方法在线学习线性攻击的参数,数值结果验证了攻击的有效性。
2020-02-04 cs.SY eess.SY math.OC
Generating Sustainability-Targeting Attacks For Cyber-Physical Systems
Texas Tech University(德克萨斯理工大学)
本文提出了一种通用数学框架,用于建模隐蔽的可持续性目标攻击,并推导出在线性网络物理系统上生成最小努力最大影响攻击的可行性条件。
2026-04-30 cs.SY eess.SY
Secure State Estimation of Cyber-Physical Systems via Gaussian Bernoulli Mixture Model
本文提出高斯-伯努利安全(GBS)估计器,将未知攻击模型下的传感器攻击检测转化为状态与观测指示符的最优估计问题,并结合卡尔曼滤波与近端梯度下降实现高效求解,实验表明其在计算效率、检测性能和估计误差上均优于现有方法。
2025-08-23 cs.SY eess.SY
REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency
University of Pennsylvania(宾夕法尼亚大学)
本文提出了一种新的模型修复方法和Matlab工具包REAFFIRM,用于通过模型修复提高车载系统(CPSs)的容错性。该方法通过混合系统模型变换和模型综合工具,基于安全要求生成修复后的模型。
2019-02-09 cs.SY eess.SY