Finding liveness 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 of model checkers found in the literature use exact deterministic algorithms to check the properties. These algorithms usually require huge amounts of memory if the checked model is large. We propose here the use of an algorithm based on ACOhg, a new kind of ant colony optimization model, to search for liveness property violations in concurrent systems. This algorithm has been previously applied to the search for safety errors with very good results and we apply it here for the first time to liveness errors. The results state that our algorithmic proposal, called ACOhg-live, is able to obtain very short error trails in faulty concurrent systems using a low amount of resources, outperforming by far the results of nested-DFS, the traditional algorithm used for this task in the model checking community and implemented in most of the explicit state model checkers. This fact makes ACOhg-live a very suitable algorithm for finding liveness errors in large faulty concurrent systems, in which traditional techniques fail because of the model size.