Abstract
Robustness testing aims at finding errors in a system under invalid conditions, such as unexpected inputs. We propose a robustness testing approach for Event-B based on specification mutation and model-based testing. We assume that a specification describes the valid inputs of a system. By applying negation rules, we mutate the precondition of events to explore invalid behaviour. Tests are generated from the mutated specification using ProB. ProB has been adapted to efficiently process mutated events. Mutated events are statically checked for satisfiability and enability using constraint satisfaction, to prune the transition search space. This has dramatically improve the performance of test generation. The approach is applied to the Java Card bytecode verifier. Large mutated specifications (containing 921 mutated events) can be easily tackled to ensure a good coverage of the robustness test space.
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
References
Abrial, J.: Modeling in Event-B. Cambridge University Press, Cambridge (2010)
Agrawal, et al.: Design of Mutant Operators for the C Programming Language. Technical report, Software Engineering Research Center, Purdue University (1989)
Aichernig, B.K., Lorber, F.: Model-based Mutation Testing with Timed Automata. Technical report IST-MBT-2013-02, TU Graz, pp. 1–21 (2013)
Bouquet, F. et al.: A subset of precise UML for model-based testing. In: 3rd International Workshop on Advances in Model-based Testing, pp. 95–104. ACM (2007)
Cavalcanti, A., Gaudel, M.-C.: Data flow coverage for circus-based testing. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 415–429. Springer, Heidelberg (2014)
Gargantini, A.: Using model checking to generate fault detecting tests. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 189–206. Springer, Heidelberg (2007)
Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649–678 (2011)
Khurshid, S., Marinov, D.: TestEra: specification-based testing of java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004)
Kim, S., Clark, J., McDermid, J.: The Rigorous Generation of Java Mutation Operators Using HAZOP. University of York, Technical report (1999)
Leuschel, M., Butler, M.: Prob: an automated analysis toolset for the b method. Int. J. Softw. Tools Technol. Transfer 10(2), 185–203 (2008)
Mikucionis, M., Larsen, K.G., Nielsen, B.: T-UPPAAL: Online model-based testing of real-time systems. In: 19\(^{th}\) Automated Software Engineering (ASE2004), pp. 396–397 (2004)
Oracle Corporation: Java Card 3 Platform Virtual Machine Specification
Oracle Corporation: Java Card SDK
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)
Savary, A., Frappier, M., Lanet, J.-L.: Detecting vulnerabilities in java-card bytecode verifiers using model-based testing. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 223–237. Springer, Heidelberg (2013)
Shafique, M., Labiche, Y.: A systematic review of state-based test tools. Int. J. Softw. Tools Technol. Transfer 17(1), 59–76 (2015)
Utting, M., Legeard, B.: Practical Model Based Testing: A Tools Approach. Kaufmann, Morgan (2007)
Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Software Testing Verification and Reliability 22(5), 297–312 (2012)
Acknowledgements
This research was supported in part by NSERC (Natural Sciences and Engineering Research Council of Canada).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Savary, A., Frappier, M., Leuschel, M., Lanet, JL. (2015). Model-Based Robustness Testing in Event-B Using Mutation. In: Calinescu, R., Rumpe, B. (eds) Software Engineering and Formal Methods. SEFM 2015. Lecture Notes in Computer Science(), vol 9276. Springer, Cham. https://doi.org/10.1007/978-3-319-22969-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-22969-0_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22968-3
Online ISBN: 978-3-319-22969-0
eBook Packages: Computer ScienceComputer Science (R0)