Logo image
Back
Controlling test case explosion in test generation from B formal models
Journal article   Peer reviewed

Controlling test case explosion in test generation from B formal models

Bruno Legeard, F Peureux and Mark Utting
Software Testing Verification and Reliability, Vol.14(2), pp.81-103
2004
DOI: https://doi.org/10.1002/stvr.287
url
https://doi.org/10.1002/stvr.287View
Published Version

Abstract

model-based testing boundary values set constraint solving B notation
BZ-TESTING-TOOLS (BZ-TT) is a tool set for automated test case generation from B and Z specifications. BZ-TT uses boundary and cause-effect testing on the basis of the formal model. It has been used and validated on several industrial applications in the domain of critical software, particularly smart card and transport systems. This paper presents the test coverage criteria supported by BZ-TT. On the one hand, these correspond to various classical structural coverage criteria, but specialized to the case of B abstract machines. The paper gives algorithms for these in Prolog. On the other hand, BZ-TT introduces new coverage criteria for complex data structures, based on boundary analysis: this paper defines weak and strong state-boundary coverage, input-boundary coverage and output-boundary coverage. Finally, the paper describes how BZ-TT presents a unified view of these criteria to the validation engineer, and allows him or her to control the test case explosion on a coarse basis (choosing from a range of coverage criteria) as well as a fine basis (selecting options for each state or input variable). © 2004 John Wiley and Sons, Ltd.

Details

Metrics

2 File views/ downloads
476 Record Views
13 Times Cited - Web of Science

InCites Highlights

These are selected metrics from InCites Benchmarking & Analytics tool, related to this output

Collaboration types
Domestic collaboration
International collaboration
Web Of Science research areas
Computer Science, Software Engineering
Logo image