Show simple item record  

dc.contributor.authorLegeard, Bruno
dc.contributor.authorPeureux, Fabien
dc.contributor.authorUtting, Mark
dc.identifier.citationLegeard, B., Peureux, F. & Utting, M.(2004). Controlling test case explosion in test generation for B formal models: Research Articles. Software Testing, Verification & Reliability, 14(2), 81-103.en_US
dc.description.abstractBZ-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).en_US
dc.publisherJohn Wiley & Sons, Ltd.en_US
dc.subjectcomputer scienceen_US
dc.subjectmodel-based testingen_US
dc.subjectboundary valuesen_US
dc.subjectset constraint solvingen_US
dc.subjectB notationen_US
dc.titleControlling test case explosion in test generation for B formal models: Research Articlesen_US
dc.typeJournal Articleen_US

Files in this item


There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record