Premium
Scenario‐based testing using symbolic animation of B models
Author(s) -
Dadeau Frédéric,
Castillos Kalou Cabrera,
Tissot Régis
Publication year - 2012
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.1467
Subject(s) - computer science , animation , symbolic execution , programming language , test case , model based testing , computer animation , software engineering , machine learning , computer graphics (images) , software , regression analysis
SUMMARY 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. Copyright © 2012 John Wiley & Sons, Ltd.