Hits:

Affiliation of Author(s):计算机科学与技术学院/人工智能学院/软件学院

Title of Paper:A PSO-Based CEGAR Framework for Stochastic Model Checking

Journal:Int. J. Software Engineer. Knowledge Engineer.

Abstract:Counterexample-guided abstraction refinement (CEGAR) is an extremely successful methodology for combating the state-space explosion problem in model checking. State-space explosion problem is more serious in the field of stochastic model checking, and it is still a challengeable problem to apply CEGAR in stochastic model checking effectively. In this paper, we formalize the problem of applying CEGAR in stochastic model checking, and propose a novel CEGAR framework for it. In our framework, the abstract model is presented by a quotient probabilistic automaton by making a set of variables or latches invisible, which can distinguish more degrees of abstraction for each variable. The counterexample is described by a diagnostic sub-model. Validating counterexample is performed on diagnostic loop paths, and the directed explicit state-space search algorithm is used for searching diagnostic loop paths. Sample learning, particle swarm optimization algorithm (PSO) and some effective heuristics are integrated for refining abstract model guided by invalid counterexample. A prototype tool is implemented for the framework, and the feasibility and efficiency are shown by some large cases. © 2019 World Scientific Publishing Company.

ISSN No.:0218-1940

Translation or Not:no

Date of Publication:2019-10-01

Co-author:Ma, Yan,Liu, Yang

Correspondence Author:Cao Zi Ning