基于3值抽象的假设-保证式PCTL*组合随机模型检验方法

Stochastic model checking is a recent extension and generalization of the classical model checking, which faces the more severe state explosion problem. Compositional stochastic model checking by assume-guarantee reasoning is a theoretically feasible way to alleviate the state explosion problem. Nevertheless, current compositional stochastic model checking by assume-guarantee reasoning can only be used to verify the probabilistic safety property (proper subset of PCTL* property), because the method for generating assumption belongs to two valued abstraction essentially. Take the generating assumption as breakthrough, we try to explore the PCTL* compositional stochastic model checking by three valued abstraction-based assume-guarantee reasoning. Specifically speaking, it includes: propose generating the assumption with three valued abstraction refinement, and maintaining it as the extended stochastic game model; study transforming the PCTL* compositional stochastic model checking into the problem of secure equilibrium for stochastic game, and using the quantum-behaved particle swarm optimization algorithm to solve it; study constructing and describing the counterexample as the annotated sub-stochastic game with the strategy information. The new approach proposed can tackle the state explosion problem in PCTL* stochastic model checking effectively, even be helpful for the PCTL* stochastic model checking infinite state system or compositional stochastic model checking by assume-guarantee reasoning for some other quantitative property specifications, and it can quantitatively verify a wide range of the component-based stochastic software system.

随机模型检验是经典模型检验理论的延伸和推广，其面临更为严重的状态爆炸问题。把假设-保证推理引入随机模型检验实现假设-保证式组合随机模型检验，是一种缓解状态爆炸问题的可行方法；但目前的假设-保证式组合随机模型检验方法因其产生假设的方式本质属于2值语义抽象范畴，只能用于验证概率安全性质(PCTL*真子集性质)。本项目以产生假设的方式为突破口，探索一种可验证PCTL*全集性质的假设-保证式组合随机模型检验方法：提出用3值抽象精化产生假设，并用扩展的随机博弈表示假设；研究将PCTL*组合随机模型检验转换为随机博弈的安全均衡问题，并用量子行为的粒子群优化算法求解；研究用标注的子随机博弈构造和表示反例。项目研究可有效缓解PCTL*随机模型检验的状态爆炸问题，对于实现PCTL*随机模型检验无限状态系统和其它定量性质的组合随机模型检验也有一定的参考意义；可广泛应用于展现随机行为的构件软件系统的定量验证。

用模型检验(model checking，也译为模型检测)的方法对具有随机行为的复杂系统进行定量的验证，简称为随机模型检验或概率模型检验。近十年，随机模型检验引起了形式验证等领域的广泛关注，取得了较大的进展。我们的研究工作可归纳为组合随机模型检验理论和应用研究两个层面，相关成果发表于CCF B类期刊、CCF C类期刊、计算机学报和软件学报等著名国内外期刊和国际会议。 . （1）理论方面：1）对随机模型检验的最基本原理进行深入研究，总结了随机模型检验的主要研究方向及其进展，归纳了随机模型检验的应用领域和其未来的应用挑战；用带有标号函数的概率Petri网（LPPN）作为随机系统的high-level模型，提出了一种PCTL*随机模型检验算法验证LPPN模型。2）把博弈理论引入PCTL*随机模型检验，实现了基于博弈的PCTL*随机模型检验算法。3）给出随机模型检验中反例必需满足的条件，提出用诊断子图表示随机模型检验的反例，并用带有启发式的粒子群优化算法求解反例。4）给出了随机模型检验中抽象技术的形式化描述，在3）反例研究工作基础上，提出一种新的面向随机模型检验的CEGAR(counterexample-guided abstraction-refinement)框架。5）把4）的精化思想用于安全飞行协议的形式化增量开发；在1）、2）、3）和4）研究工作基础上，对其进行改造，并和3值抽象相结合实现组合随机模型检验，提出一种假设保证式PCTL*组合随机模型检验算法。. （2）应用方面：将随机模型检验应用于服务流程（服务组合）的可信验证。1）用并行化方法改进HQPSO算法给出了一种可信服务流程的构造方法。2）给出了可信服务流程的非确定概率Petri网（NPPN）形式语义，提出用asPCTL随机模型检验验证其可信性质。3）将NPPN作为工作流的形式化模型，把随机模型检验验证模块集成于工作流引擎，给出了一种工作流引擎驱动的通用产品生命周期管理系统的四层架构模型。. 本项目的研究可有效地缓解PCTL*随机模型检验中的状态爆炸问题，提高PCTL*随机模型检验的可扩展性；其研究成果用于保障可信服务流程式软件的实施，丰富可信软件理论的研究。