A safety checking algorithm with multi-swarm particle swarm optimization
Tsutomu Kumazawa, Munehiro Takimoto, Yasushi Kambayashi · Proceedings of the Genetic and Evolutionary Computation Conference Companion · 2022
Model checking is a formal verification technique that automatically decides whether a software system conforms to its specification or not. One of the important features of model checking is to output a counterexample, if a violative execution is detected. Traditional exhaustive techniques fail to complete the verification in large-scale systems because of the shortage of computational resources. This is an efficiency problem called State Explosion Problem. On the other hand, the user of model checking hopes to obtain comprehensible and short outputs. However, balancing efficiency and comprehensibility is not easy, since the exhaustive investigation of the system executions is necessary to find a short counterexample. In this paper, we tackle the balancing problem with an approach of Search-Based Software Engineering. We propose a novel verification algorithm using multi-swarm Particle Swarm Optimization. Our technical breakthrough is to use the specification to decompose the verification problem into the small-sized subproblems dynamically. Each swarm solves one of the subproblems efficiently and the aggregation of the partial solutions found by the swarms provides us with sufficiently short counterexamples. Our numerical experiments show that the proposed algorithm outperforms traditional exhaustive techniques and state-of-the-art non-exhaustive techniques in terms of both efficiency and comprehensibility.