Skip to Main content Skip to Navigation
Conference papers

Model-Based Robustness Testing in Event-B Using Mutation

Abstract : Robustness testing aims at finding errors in a system under invalid conditions, such as unexpected inputs. We propose a robust-ness 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.
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-01250594
Contributor : Jean-Louis Lanet <>
Submitted on : Tuesday, January 5, 2016 - 8:52:02 AM
Last modification on : Wednesday, February 10, 2021 - 12:30:02 PM
Long-term archiving on: : Thursday, April 7, 2016 - 2:56:51 PM

File

SEFM-2015_Article.pdf
Files produced by the author(s)

Identifiers

Citation

Aymerick Savary, Marc Frappier, Michael Leuschel, Jean-Louis Lanet. Model-Based Robustness Testing in Event-B Using Mutation. SEFM 2015 - 13th International Conference Software Engineering and Formal Methods, Jan 2015, York, United Kingdom. pp.132-147, ⟨10.1007/978-3-319-22969-0_10⟩. ⟨hal-01250594⟩

Share

Metrics

Record views

646

Files downloads

693