基于切片技术的复杂模型验证方法

摘要

针对模型检测中的状态空间爆炸问题,提出一种基于带资源消耗的复杂概率迁移系统模型的性质验证方法.使用PRCTL进行模型语义逻辑表示,对迁移步数约束采用基于栈的深度遍历算法完成检验,针对冗余的迁移和状态实施二次约减,完成复杂的概率迁移系统的模型简化;针对简化后的迁移图进行概率矩阵迭代运算以判定概率条件,同时完成资源条件的判定,并进行相应的实例分析.该模型验证方法能够在一定程度上缓解复杂系统带来的状态冗余和计算繁琐问题,为性质验证工作提供了新的思路.