Abstract
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 Ant Colony Optimization (ACO) 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 results state that ACO 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 them suitable for checking safety properties in large concurrent systems, in which traditional techniques fail to find errors because of the model size.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 1–17 (1997)
Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2004)
Dorigo, M., Stützle, T.: Ant Colony Optimization. The MIT Press, Cambridge (2004)
Blum, C., Roli, A.: Metaheuristics in combinatorial optimization: Overview and conceptual comparison. ACM Computing Surveys 35(3), 268–308 (2003)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)
Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. Second SPIN Workshop, American Mathematical Society, pp. 23–32 (1996)
Edelkamp, S., Lafuente, A.L., Leue, S.: Directed Explicit Model Checking with HSF-SPIN. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)
Alba, E., Troya, J.: Genetic Algorithms for Protocol Validation. In: Proceedings of the PPSN IV International Conference, pp. 870–879. Springer, Berlin (1996)
Godefroid, P., Khurshid, S.: Exploring very large state spaces using genetic algorithms. Intl. Jnl. on Software Tools for Technology Transfer 6(2), 117–127 (2004)
Leguizamón, G., Michalewicz, Z.: A new version of Ant System for subset problems. In: Angeline, P., Michalewicz, Z., Schoenauer, M., Yao, X., Zalzala, A. (eds.) Proceedings of the 1999 Congress on Evolutionary Computation, pp. 1459–1464. IEEE Computer Society Press, Piscataway, New Jersey (1999)
Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. International Journal of Software Tools for Technology Transfer 5, 247–267 (2004)
Alba, E. (ed.): Parallel Metaheuristics. A New Class of Algorithms. Wiley, Chichester (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alba, E., Chicano, F. (2007). Ant Colony Optimization for Model Checking. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds) Computer Aided Systems Theory – EUROCAST 2007. EUROCAST 2007. Lecture Notes in Computer Science, vol 4739. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75867-9_66
Download citation
DOI: https://doi.org/10.1007/978-3-540-75867-9_66
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75866-2
Online ISBN: 978-3-540-75867-9
eBook Packages: Computer ScienceComputer Science (R0)