Abstract
Event-B is a formal modeling language having set theory as its mathematical foundation and abstract state machines as its behavioral specifications. The language has very good tool support based on theorem proving and model checking technologies, but very little support for test generation. Motivated by industrial interest in the latter domain, this paper presents an approach based on genetic algorithms that generates test data for Event-B test paths. For that, new fitness functions adapted to the set-theoretic nature of Event-B are devised. The approach was implemented and its efficiency was proven on a carefully designed benchmark using statistically sound evaluations.
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
Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)
Arcuri, A., Briand, L.: A practical guide for using statistical tests to assess randomized algorithms in software engineering. In: Proc. ICSE (to appear, 2011)
Binder, R.V.: Testing Object-Oriented Systems: Models, Patterns, and Tools, Object Technology. Addison-Wesley, London (1999)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Derderian, K., Hierons, R.M., Harman, M., Guo, Q.: Estimating the feasibility of transition paths in extended finite state machines. Autom. Softw. Eng. 17(1), 33–56 (2010)
Goldberg, D.E., Deb, K.: A comparative analysis of selection schemes used in genetic algorithms. In: FOGA, pp. 69–93 (1990)
Meffert, K., et al:. JGAP - Java Genetic Algorithms and Genetic Programming Package, http://jgap.sf.net (last visited March 2011)
Lefticaru, R., Ipate, F.: Functional search-based testing from state machines. In: Proc. ICST 2008, pp. 525–528. IEEE Computer Society Press, Los Alamitos (2008)
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)
McMinn, P.: Search-based software test data generation: A survey. Softw. Test. Verif. Reliab. 14(2), 105–156 (2004)
McMinn, P., Holcombe, M.: Evolutionary testing of state-based programs. In: GECCO 2005: Proceedings of the 2005 conference on Genetic and evolutionary computation, pp. 1013–1020. ACM, New York (2005)
Michalewicz, Z.: Genetic algorithms + data structures = evolution programs (3rd ed.). Springer, London (1996)
Mitchell, M.: An Introduction to Genetic Algorithms. MIT Press, Cambridge (1998)
Satpathy, M., Butler, M., Leuschel, M., Ramesh, S.: Automatic Testing from Formal Specifications. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 95–113. Springer, Heidelberg (2007)
Sheskin, D.J.: Handbook of Parametric and Nonparametric Statistical Procedures, 4th edn. Chapman & Hall/CRC (2007)
Stefanescu, A., Ipate, F., Lefticaru, R., Tudose, C.: Towards search-based testing for Event-B models. In: Proc. of 4th Workshop on Search-Based Software Testing (SBST 2011). IEEE, Los Alamitos (to appear, 2011)
Tracey, N.J.: A Search-based Automated Test-Data Generation Framework for Safety-Critical Software. PhD thesis, University of York (2000)
Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann Publishers Inc, San Francisco (2006)
Wieczorek, S., Kozyura, V., Roth, A., Leuschel, M., Bendisposto, J., Plagge, D., Schieferdecker, I.: Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models. In: Núñez, M., Baker, P., Merayo, M.G. (eds.) TESTCOM 2009. LNCS, vol. 5826, pp. 179–194. Springer, Heidelberg (2009)
Yano, T., Martins, E., de Sousa, F.L.: Generating feasible test paths from an executable model using a multi-objective approach. In: Proc. ICSTW 2010, pp. 236–239. IEEE Computer Society, Los Alamitos (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dinca, I., Stefanescu, A., Ipate, F., Lefticaru, R., Tudose, C. (2011). Test Data Generation for Event-B Models Using Genetic Algorithms. In: Zain, J.M., Wan Mohd, W.M.b., El-Qawasmeh, E. (eds) Software Engineering and Computer Systems. ICSECS 2011. Communications in Computer and Information Science, vol 181. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22203-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-22203-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22202-3
Online ISBN: 978-3-642-22203-0
eBook Packages: Computer ScienceComputer Science (R0)