Counterexample Generation in Stochastic Model Checking Based on PSO Algorithm with Heuristic
| Autor: | Zining Cao, Yang Liu, Yan Ma |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Model checking
Mathematical optimization Computer Networks and Communications Computer science Particle swarm optimization 020207 software engineering 0102 computer and information sciences 02 engineering and technology Heuristic function 01 natural sciences Computer Graphics and Computer-Aided Design 010201 computation theory & mathematics Artificial Intelligence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Witsenhausen's counterexample 0202 electrical engineering electronic engineering information engineering Stochastic model checking Software Coding (social sciences) Counterexample |
| Zdroj: | International Journal of Software Engineering and Knowledge Engineering. 26:1117-1143 |
| ISSN: | 1793-6403 0218-1940 |
| DOI: | 10.1142/s021819401650039x |
| Popis: | Providing counterexample for the refutation of a property is an essential feature of model checking, if it is not the most important. However, generating counterexample in stochastic model checking needs a dedicated algorithm. It usually costs too much time and memory, and sometimes it cannot find the counterexample. What is worse, generating smallest counterexample in stochastic model checking has been proved to be NP-complete, and it is unlikely to be efficiently approximable. Although there are a few heuristic methods that are applied to the construction of the counterexample, it is usually difficult to determine the heuristic function which is critical for counterexample generating. In this paper, we present a particle swarm optimization (PSO)-based approach to generating counterexample for stochastic model checking. We define the diagnostic sub-graph as counterexample, and extend PSO algorithm with heuristic (HPSO) to generate counterexample. It adopts indirect path coding scheme to expand the scope of the search space, and employs heuristic operator to generate more effective path. The validity of our approach is illustrated by some case studies in a prototype tool. The experiments show that HPSO algorithm can significantly outperform the present algorithm for counterexample generation in stochastic model checking. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|