概率 B 中定量安全精化的模型探索与分析
计算机科学中的逻辑
2011-06-22 v1 软件工程
摘要
反例在标准系统分析中所扮演的角色是众所周知的；但在概率系统精化中，反例的概念则不那么常见。本文扩展了先前利用反例研究概率系统归纳不变性质的工作，展示了如何利用反例来扩展有界模型检测风格的分析技术，以用于概率 B 语言中定量安全规约的精化。特别地，我们展示了该方法如何适配包含概率循环的精化。最后，我们在 pB 模型上演示了该技术，这些模型总结了一个用于寻找无向图最小割的随机化算法的一步精化，以及一个控制器设计的可信性分析。
引用
@article{arxiv.1106.4096,
title = {Model exploration and analysis for quantitative safety refinement in probabilistic B},
author = {Ukachukwu Ndukwu and Annabelle McIver},
journal= {arXiv preprint arXiv:1106.4096},
year = {2011}
}
备注
In Proceedings Refine 2011, arXiv:1106.3488