Model-Based Robustness Testing in Event-B Using Mutation

Aymerick Savary 1, 2 Marc Frappier 2 Michael Leuschel 3 Jean-Louis Lanet 4
1 UNILIM - Université de Limoges
2 GRIL - Groupe de Recherche en Ingénierie du Logiciel [Sherbrooke]
Département d'informatique [Sherbrooke]
3 Heinrich-Heine-Universität Düsseldorf [Düsseldorf]
4 TAMIS - Threat Analysis and Mitigation for Information Security
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Keywords : Robustness Testing Specification Mutation Model-Based Testing Vulnerability Analysis Intrusion Testing Event-B ProB
Type de document :
Communication dans un congrès
Radu Calinescu; Bernhard Rumpe SEFM 2015 - 13th International Conference Software Engineering and Formal Methods, Jan 2015, York, United Kingdom. Springer, Lecture Notes in Computer Science Volume 9276 (Volume 9276 ), pp.132-147, 2015, Software Engineering and Formal Methods. 〈10.1007/978-3-319-22969-0_10〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01250594
Contributeur : Jean-Louis Lanet <>
Soumis le : mardi 5 janvier 2016 - 08:52:02
Dernière modification le : jeudi 7 février 2019 - 16:02:00
Document(s) archivé(s) le : jeudi 7 avril 2016 - 14:56:51

Fichier

SEFM-2015_Article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UNILIM | IRISA | CENTRALESUPELEC | UR1-UFR-ISTIC | UNIV-RENNES | IRISA-D4

Citation

Aymerick Savary, Marc Frappier, Michael Leuschel, Jean-Louis Lanet. Model-Based Robustness Testing in Event-B Using Mutation. Radu Calinescu; Bernhard Rumpe SEFM 2015 - 13th International Conference Software Engineering and Formal Methods, Jan 2015, York, United Kingdom. Springer, Lecture Notes in Computer Science Volume 9276 (Volume 9276 ), pp.132-147, 2015, Software Engineering and Formal Methods. 〈10.1007/978-3-319-22969-0_10〉. 〈hal-01250594〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

379

Téléchargements de fichiers

187

Contact


archive-ouverte@inria.fr