Searching for liveness property violations in concurrent systems with ACO

Liveness properties in concurrent systems are, informally, those properties that stipulate that something good eventually happens during execution. In order to prove that a given system satisfies a liveness property, model checking techniques are utilized. However, most of the model checkers found in the literature use exhaustive deterministic algorithms that require huge amounts of memory if the concurrent system is large. Here we propose the use of an algorithm based on ACOhg, a new kind of Ant Colony Optimization algorithm, for searching for liveness property violations in concurrent systems. We also take into account the structure of the liveness property in order to improve the efficacy and efficiency of the search. 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 and Improved-Nested-DFS, two algorithms used in ...

• Type: Conference
• Year: 2008
• Where: GECCO
• Authors: Enrique Alba, J. Francisco Chicano
• Keywords: Concurrent Systems, Faulty Concurrent Systems, GECCO 2008, Liveness Property, Optimization