Model checking is a formal and automated verification technique to show that a software system behaves in accordance with the given specification. Traditional model checking uses exhaustive search techniques for finding violative behaviours of the specification. The techniques, however, often do not work for huge systems because it demands a huge amount of computational resources. Search-Based Software Engineering is known to effectively solve many software engineering problems including model checking. It pursues the good balance between efficiency and qualities of solutions by using swarm intelligence and metaheuristic search methodologies. This article focuses on the state-of-the-art model checking with Ant Colony Optimization. Ant Colony Optimization is a metaheuristic, population-based and stochastic optimization algorithm. We propose two exploration strategies to further improve the balance in model checking based on Ant Colony Optimization. The proposed strategies introduce different kinds of randomized selection mechanisms to diversify solutions found by many agents. The strategies help the search algorithm extend the reachable regions effectively. Through numerical experiments, we confirmed that the proposed strategies require less computation time and memory as compared to the existing model checking with Ant Colony Optimization at the cost of finding slightly less qualified solutions.

In software engineering, errors or faults in software systems often lead to critical social problems. One effective methodology to tackle this problem is model checking, which is an automated formal verification technique. In traditional model checking, the task of finding specification errors is reduced to deterministic search techniques such as Depth-First Search. Recent research has shown that swarm intelligence offers a powerful search capability compared to traditional techniques. In particular, multi-swarm Particle Swarm Optimization is known to be efficient and can mitigate the state-space explosion problem, i.e., the exponential increase in the search space with a linear increase in the problem size. However, the state-space explosion problem is still significant when verifying very large systems. Further performance improvement is needed. To achieve this, we propose a novel memoization or cache mechanism for storing tentative solutions for reuse in the later stages of the search procedure. For each stage, a candidate solution computed by a swarm is summarized efficiently and heuristically to consolidate similar solutions into a single representative solution. We store the summary and its associated solutions in key-value maps. Instead of computing known solutions repeatedly, we retrieve the solution if the stored key matches the summary. We incorporated the proposed mechanism into a model-checking technique with multi-swarm Particle Swarm Optimization and evaluated the search performance. We show in this paper that the proposed mechanism improved time and space consumption while maintaining solution quality.