Page 164 - 《软件学报》2025年第8期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(8):3587−3603 [doi: 10.13328/j.cnki.jos.007352] [CSTR: 32375.14.jos.007352] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
基于混成自动机路径过滤与动态选择的 CPS 系统反例生成

王佳宛 1,2 , 刘熹橦 2 , 卜 磊 1,3 , 李宣东 1,2

(计算机软件新技术全国重点实验室 (南京大学), 江苏 南京 210023)
1
2
(南京大学 计算机学院, 江苏 南京 210023)
3
(南京大学 软件学院, 江苏 南京 210093)
通信作者: 卜磊, E-mail: bulei@nju.edu.cn

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

中文引用格式: 王佳宛, 刘熹橦, 卜磊, 李宣东. 基于混成自动机路径过滤与动态选择的CPS系统反例生成. 软件学报, 2025, 36(8):
3587–3603. http://www.jos.org.cn/1000-9825/7352.htm
英文引用格式: Wang JW, Liu XT, Bu L, Li XD. CPS Falsification Based on Hybrid Automata Path Filtering and Dynamic Selection.
Ruan Jian Xue Bao/Journal of Software, 2025, 36(8): 3587–3603 (in Chinese). http://www.jos.org.cn/1000-9825/7352.htm

CPS Falsification Based on Hybrid Automata Path Filtering and Dynamic Selection
1,3
2
1,2
WANG Jia-Wan , LIU Xi-Tong , BU Lei , LI Xuan-Dong 1,2
1
(State Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210023, China)
2
(School of Computer Science and Technology, Nanjing University, Nanjing 210023, China)
3
(Software Institute, Nanjing University, Nanjing 210093, China)
Abstract: Cyber-physical system (CPS) is widely employed in safety-critical domains, making its safety assurance a critical concern.
Formal verification serves as an effective approach for proving system safety but encounters challenges when applied to complex real-
world CPS. Falsification has been proposed as an alternative, aiming to demonstrate system unsafety by identifying counterexample
behaviors that violate specified safety properties. Existing path-oriented falsification methods for CPS utilize divide-and-conquer strategies
to explore system behaviors along individual paths, effectively uncovering unsafe behaviors. However, in large-scale CPS, these methods
are hindered by the path explosion problem, where the number of paths grows exponentially with the system’s discrete system modes,
leading to significant reductions in falsification efficiency and performance. To address the path explosion issue in path-oriented
falsification, this study introduces two novel techniques based on system models and specifications: path filtering and dynamic path

* 基金项目: 国家自然科学基金 (62232008, 62172200); 江苏省前沿引领技术基础研究专项 (BK20202001)
本文由“形式化方法与应用”专题特约编辑陈明帅研究员、田聪教授、熊英飞副教授推荐.
收稿时间: 2024-08-26; 修改时间: 2024-10-14; 采用时间: 2024-11-26; jos 在线出版时间: 2024-12-10
CNKI 网络首发时间: 2025-04-03