随机模型检验研究

摘要：

随机模型检验作为模型检验理论的延伸和推广，可用于验证分析系统模型的定性或定量性质，其已经应用到随机分布式算法验证、通信协议性能分析甚至是系统生物学等跨学科领域。从20世纪90年代末至今，随机模型检验引起了形式验证等领域的广泛关注，并取得了很大的进展。该文追溯了随机模型检验的渊源，系统地概括了其最基本的原理及几类典型的 PCTL、概率的 LTL、PCTL*和 CSL 模型检验随机系统的算法框架。然后归纳总结了随机模型检验的主要研究方向及其进展，分析了基于随机模型检验的验证过程及其优势与劣势，并分类列出了目前出现的随机模型检验工具。最后介绍了随机模型检验的应用领域并指出了其未来的应用挑战。

关键词：形式验证、马尔可夫随机过程、随机模型检验、定量分析

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目61303022，91318301;中国博士后科学基金项目2013M531328;山东省自然科学基金项目ZR2012FQ013;山东省高等学校科技计划项目J13LN10;山东省泰安市科技发展计划项目201330629资助。

在线出版日期：2015-12-09（万方平台首次上网日期，不代表论文的发表时间）

页数：共18页

页码：2145-2162