用可观测系统特征改进贝叶斯推理，提升软件验证准确性
Leveraging System-Level Observations to Inform Bayesian Learning of Model Parameters for Quantitative Verification
- 通过可观察的系统级属性推导模型参数先验分布
- 在多个真实案例中验证了对难测性质的准确分析能力
- 适合依赖领域知识但缺乏精确参数的验证场景
结合贝叶斯学习与定量验证是分析软件系统关键量化属性（如可靠性、响应时间）的强大工具。然而，验证结果的准确性和鲁棒性强烈依赖于贝叶斯推断背后的先验知识（PK）。该知识反映对事件概率的初始信念，通常依赖领域经验。使用不准确或非信息性的先验知识会负面影响定量分析，导致错误的验证结果。本文提出的EPIK方法通过提取并嵌入先验知识，解决这一挑战。与以往需在形式化模型转移参数上定义先验的方法不同，EPIK利用直接可观测的系统级属性，这些属性具有真实世界语义关联。EPIK构建双重优化问题以推导未知转移参数的分布，并将这些分布用于验证新出现或难以测量（隐晦）的性质。通过多个真实案例变体及多种EPIK实例的详细实验评估，证明了其有效性、灵活性与通用性。
原文摘要 · Abstract (English)
Combining Bayesian learning and quantitative verification is a powerful toolset for analysing key quantitative properties of software systems, like reliability and response time. However, the accuracy and robustness of verification results strongly depend on the prior knowledge (PK) underlying Bayesian inference. This knowledge reflects original beliefs about the probability of events and typically depends on domain expertise. Using inaccurate or uninformative PK can negatively affect quantitative analysis, yielding incorrect verification results. Our EPIK approach tackles this important challenge by eliciting and embedding PK in quantitative verification equipped with Bayesian estimators. Unlike existing approaches that require PK on formal model transition parameters, EPIK leverages system-level properties that are directly observable and are linked to real-world semantics. EPIK formulates a twofold optimisation problem to derive the distributions of unknown transition parameters and then embeds these distributions to verify new or difficult-to-measure (elusive) properties. The detailed experimental evaluation using multiple variants of real-world case studies and diverse EPIK instantiations shows its effectiveness, flexibility and generality.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。