Scenario-Based Testing using Symbolic Animation of B Models

Frédéric Dadeau 1, 2 Kalou Cabrera Castillos 2, 1 Régis Tissot 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This article presents a model-based test generation technique, from user-defined scenarios, for behavioral models expressed as B machines. Scenarios are expressed using a customized formalism, based on regular expressions, that makes it possible to describe sequences of operation calls possibly reaching specific states of the system. A symbolic animation engine, simulating the execution of a model using constraint logic programming, is then exploited to play the unfolded scenarios on the model and to instantiate the test cases, providing the expected results used to establish the conformance verdict. This approach is tool supported by a research prototype and has been successfully applied in an industrial context of a smart card applet. This tool is extended by a scenario generator, which automatically generates testing strategies for exercising user-defined properties, written using specific patterns
Type de document :
Article dans une revue
Software Testing, Verification and Reliability, Wiley, 2012, 6 (22), pp.407-434. 〈10.1002/stvr.1467〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00760020
Contributeur : Frédéric Dadeau <>
Soumis le : lundi 3 décembre 2012 - 12:21:59
Dernière modification le : jeudi 11 janvier 2018 - 06:24:26

Identifiants

Citation

Frédéric Dadeau, Kalou Cabrera Castillos, Régis Tissot. Scenario-Based Testing using Symbolic Animation of B Models. Software Testing, Verification and Reliability, Wiley, 2012, 6 (22), pp.407-434. 〈10.1002/stvr.1467〉. 〈hal-00760020〉

Partager

Métriques

Consultations de la notice

313