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

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

项目编号： No.61303022

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 刘阳

作者单位： 泰山学院

项目金额： 26万元

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

英文关键词： stochastic model checking；game；counterexample；assume-guarantee reasoning；trustworthy service flow