基于混成自动机路径过滤与动态选择的CPS系统反例生成
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

卜磊,E-mail:bulei@nju.edu.cn

中图分类号:

TP311

基金项目:

国家自然科学基金(62232008,62172200);江苏省前沿引领技术基础研究专项(BK20202001)


CPS Falsification Based on Hybrid Automata Path Filtering and Dynamic Selection
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    信息物理融合系统(Cyber-Physical Systems, CPS)在安全攸关领域具有广泛的应用,保障其安全性至关重要.形式化验证是证明系统安全性的有效手段,但在现实世界中的复杂CPS系统上应用仍面临挑战.因此,反例生成的方法被提出,旨在通过寻找系统中违背安全规约的反例行为来证明系统的不安全.现有的基于路径的CPS系统反例生成方法采用分治策略,针对系统模型中各条路径上的行为空间分别进行探索,能够有效发现系统中的不安全行为.然而,在大规模系统中,这类方法面临严重的路径爆炸问题,路径数量随着离散状态数目指数级增长,反例生成的效率和性能显著下降.为缓解反例生成中的路径爆炸问题,本文基于系统模型与规约提出了路径过滤与动态选择两种技术.首先,我们设计面向规约的路径过滤方法,通过分析系统规约的语法树和路径上的行为约束,快速过滤不可能包含不安全行为的路径.其次,我们引入多臂老虎机算法来指导反例生成过程中路径的动态选择,动态调整用于探索不同路径的计算资源以最大化反例生成的性能.在一系列经典测试案例上的实验结果表明,我们的方法显著缓解了路径爆炸问题,提高了CPS系统反例生成的效率和性能,将发现不安全行为的成功率提升了两倍以上.

    Abstract:

    Cyber-Physical Systems (CPS) find extensive applications in safety-critical domains, making it crucial to ensure their safety. Formal verification is a powerful technique for proving system safety, but its application in complex, real-world CPS remains challenging. Falsification is therefore proposed, which aims to prove the unsafety of a system by identifying counterexample system behaviors that violate given safety properties. Existing path-oriented CPS falsification methods employ divide-and-conquer strategies, exploring system behavior along system paths, and can discover unsafe behaviors effectively. However, in large-scale CPSs, these methods face the serious challenge of path explosion. As the number of discrete system modes increases, the number of paths grows exponentially, leading to a notable decrease in falsification efficiency and performance. To mitigate the path explosion problem during path-oriented falsification, this paper proposes two techniques based on the system model and specification: path filtering and dynamic path selection. Firstly, we introduce a specification-driven path filtering technique that rapidly filters out paths unlikely to contain unsafe behaviors by analyzing the syntax tree of system specifications and the constraints on behaviors along each path. Secondly, we employ a multi-armed bandit algorithm to dynamically select paths to be falsified during the falsification process, adaptively adjusting computational resources allocated to explore different paths to maximize performance. Experimental results on a series of classical benchmarks show that our techniques significantly alleviate the path explosion issue and improve CPS falsification performance, leading to a twofold increase in the success rate of identifying unsafe system behaviors.

    参考文献
    相似文献
    引证文献
引用本文

王佳宛,刘熹橦,卜磊,李宣东.基于混成自动机路径过滤与动态选择的CPS系统反例生成.软件学报,2025,36(8):0

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2024-08-26
  • 最后修改日期:2024-10-14
  • 录用日期:
  • 在线发布日期: 2024-12-10
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号