Finding safety errors with ACO

Model Checking is a well-known and fully automatic technique for checking software properties, usually given as temporal logic formulae on the program variables. Most model checkers found in the literature use exact deterministic algorithms to check the properties. These algorithms usually require huge amounts of computational resources if the checked model is large. We propose here the use of a new kind of Ant Colony Optimization (ACO) model, ACOhg, to refute safety properties in concurrent systems. ACO algorithms are stochastic techniques belonging to the class of metaheuristic algorithms and inspired by the foraging behaviour of real ants. The traditional ACO algorithms cannot deal with the model checking problem and thus we use ACOhg to tackle it. The results state that ACOhg algorithms find optimal or near optimal error trails in faulty concurrent systems with a reduced amount of resources, outperforming algorithms that are the state-of-the-art in model checking. This fact makes ...

• Type: Conference
• Year: 2007
• Where: GECCO
• Authors: Enrique Alba, J. Francisco Chicano
• Keywords: ACO Algorithms, Algorithms, GECCO 2007, Model Checking, Optimization