by Francisco Chicano and Enrique Alba
Mimicking the behaviour of ants in nature can lead to the identification of subtle errors in concurrent software systems and thereby boost the efficiency of model checking.
Testing, verification and validation methods are especially important in safety-critical software, such as airplane controllers, nuclear power plant control systems, and medical tools software. Much effort has been devoted to developing and improving such methods. The main goal of all this research is to obtain a practical software tool that is able to automatically answer the following questions: (1) does my software system fulfil the specification?, and (2) if not, why not?
One method that automatically approaches both questions is model checking. This well-known and fully automatic formal procedure analyses all possible program states (explicitly or implicitly) in order to prove whether or not a given concurrent system satisfies a property like, for example, the absence of deadlocks, the absence of starvation, matching an invariant etc. The main drawback of model checking is the so-called state explosion. The memory required for the verification usually grows exponentially with the size of the system being verified. This fact limits the size of the systems that model checkers can actually verify, making the procedure impractical in large (real) software systems.
Memory poses a challenge to formal methods if we want them to be able to answer the first question, but the memory requirement can be relaxed if we focus on the second question, that is, if we focus on the search for error traces in the software. In effect, if the software system contains an error, a guided search can discover the error without having to explore the entire state space of the system. This approach is especially useful in the initial and middle stages of software development and after any maintenance modification, in which the answer to the first question is most probably "no".
In this context we recently started a new research line in our research group at the University of Málaga (Spain), using Ant Colony Optimization (ACO) algorithms to search for error traces in concurrent software systems. ACO algorithms are inspired by the foraging behaviour of real ants. These algorithms are a subclass of metaheuristic algorithms, a well-known set of techniques for finding near-optimal solutions to NP-hard optimization problems using a reasonable amount of computational resources.
In short, the core of our approach is to simulate the ants' behaviour in a graph: the state graph of the software system. The objective of the artificial ants is to find error states in the graph by employing the same mechanisms used by real ants to find food in a real environment (see Figure 1). These mechanisms include indirect information exchange through chemicals (pheromone trail) and external guidance (heuristic information). This heuristic information is automatically computed from the property being checked (eg from the temporal logic formula). Artificial ants traverse the state graph, jumping from one state to another using arcs that represent transitions in the software system. In each jump, ants must select one of several successor states using the pheromone trail (deposited by previous ants) and the heuristic information associated with them. In making this selection, ants prefer the states that suggest paths most likely to lead to an error state. When a state is found that violates the software specification, an error is reported along with its corresponding error trace (ant path).
The idea described in the previous paragraph has proven to be very effective in practice. The results show that this approach requires a minimal amount of memory (tens of megabytes at most), even in large software systems. In fact, in software systems for which other algorithms traditionally used in the model checking community (eg Nested Depth First Search) fail due to memory constraints to find any error traces, this method succeeds. And yet low memory use is not the only advantage of ACO algorithms. As happens with real ants in nature, ACO algorithms exhibit the property of finding short paths to the target. This means short error traces, which are very useful during the software development phases, since shorter error traces can be more easily understood by the programmers. Significant advantages in memory utilization and error trace length reduction can be derived from the use of advanced algorithms like ACO rather than traditional methods, especially when the goal is to look for violations of the specification in actual software.
Encouraged by the results obtained so far, we have identified several lines to follow in the near future. First, we are studying how to integrate our proposal with software tools for automatic testing and verification (already completed for SPIN and Java PathFinder). This could save a great deal of testing time in software companies. Second, we are investigating the application of other algorithms inspired by nature, like Particle Swarm Optimization or Simulated Annealing. And last but not least, we would like to use ACO algorithms to answer the first question: does the software system fulfil the specification?
Link:
http://neo.lcc.uma.es
Please contact:
Francisco Chicano
University of Málaga, Spain
Tel: +34 95213 2815
E-mail: chicano
lcc.uma.es
Enrique Alba
University of Málaga, Spain
Tel: +34 95213 2803
E-mail: eatlcc.uma.es
