发表机构
Cyprus University of Technology; Wuhan University（塞浦路斯理工大学; 武汉大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出EPIK方法，利用可观测的系统级属性替代需形式化模型转移参数的先验知识，构建双重优化问题推导参数分布以验证属性，经实验证明其有效灵活通用。
AI 中文摘要
将贝叶斯学习与定量验证相结合，是分析软件系统可靠性、响应时间等关键定量属性的强大工具集。然而，验证结果的准确性与鲁棒性高度依赖贝叶斯推理所基于的先验知识（PK），该知识反映了对事件概率的初始信念，通常依赖领域专业知识。使用不准确或无信息的PK会对定量分析产生负面影响，导致验证结果错误。我们的EPIK方法解决这一重要挑战，通过提取PK并将其嵌入配备贝叶斯估计器的定量验证中。与现有需要形式化模型转移参数上PK的方法不同，EPIK利用可直接观测且与现实语义关联的系统级属性。EPIK构建双重优化问题以推导未知转移参数的分布，随后将这些分布嵌入以验证新的或难以测量（难以捉摸）的属性。通过现实案例研究的多个变体和不同EPIK实例化的详细实验评估，证明了其有效性、灵活性和通用性。
英文摘要
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.
Comments11 pages, 9 figures
