paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Parametric Falsification of Many Probabilistic Requirements Under Flakiness

抖动下多概率需求的参数化证伪
ICSE 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE)2025匹配度 2/10 · 论文属于形式化方法与测试领域,研究概率需求的参数化模型检测与多目标优化证伪,但未涉及LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户核心研究方向(PL与AI交叉、浮点/贝叶斯程序分析)关联较弱。引用 1 inbox
Matteo Camilli, Raffaela Mirandola
crossref: 2026-09-12

AI 速览

一句话:提出结合参数化模型检测与多目标优化的方法,在抖动模拟下同时证伪多个概率需求。

证伪是基于模拟的CPS测试方法,但抖动模拟下同时检测多个可能独立需求的违反仍是开放问题。本文提出结合参数化模型检测与多目标优化的新方法:利用参数化模型检测离线预计算所有需求满足的数值约束,将部分复杂度转移至离线;再用多目标优化探索测试场景中变化因素的空间,将参数推出预计算约束,从而检测抖动违反。在四个复杂度递增的开源评估对象上,该方法能同时证伪多个需求且不掩盖个体贡献,在违反数量和严重性上显著优于随机搜索及两个SOTA基线,且额外离线计算成本可忽略。

问题
在抖动(flaky)模拟下,如何同时检测多个可能独立概率需求的违反,且不掩盖各需求的个体贡献。
方法
结合参数化模型检测与多目标优化:参数化模型检测离线预计算所有需求满足的数值约束,多目标优化在线探索场景变化因素,推动参数违反所有约束以检测抖动违反。
评估
在四个复杂度递增的开源评估对象上进行实证评估,与随机搜索和两个SOTA基线对比。结果表明在违反数量和严重性上显著更优,且额外离线计算成本可忽略。
原文摘要(Abstract)

Falsification is a popular simulation-based testing method for Cyber-Physical Systems to find inputs that violate a formal requirement. It employs optimization algorithms to minimize a robustness metric that defines the satisfaction of a given property over an execution trace. Despite falsification representing an established approach, detecting violations considering many, possibly independent, requirements simultaneously, under flaky simulations is an open problem. We address this problem by proposing a novel approach that combines parametric model checking and many-objective optimization. We use parametric model checking to shift part of the complexity of the problem offline. We pre-compute numeric constraints for the satisfaction of all requirements on a parametric specification of the testing scenario. Flaky violations are then detected using many-objective optimization to explore the space of changing factors in the scenario and push the parameters out of all precomputed constraints. The results of our empirical evaluation using four open-source evaluation subjects with increasing complexity (number of requirements) show that our approach can falsify many requirements simultaneously, without hiding their individual contribution. The effectiveness, in terms of quantity and severity of violations, is significantly higher than random search as well as two selected state-of-the-art baseline approaches. Furthermore, the extra offline computation yields a negligible cost.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot8776,
  title = {Parametric Falsification of Many Probabilistic Requirements Under Flakiness},
  author = {Matteo Camilli and Raffaela Mirandola},
  booktitle = {ICSE},
  year = {2025},
  doi = {10.1109/icse55347.2025.00237}
}