Automated boundary testing from Z and B

Bruno Legeard; Fabien Peureux; Mark Utting

doi:10.1007/3-540-45614-7_2

Back

Book chapter

Peer reviewed

Automated boundary testing from Z and B

Bruno Legeard, Fabien Peureux and Mark Utting

Formal Methods Europe 2002: Getting IT Right, pp.21-40

International Symposium of Formal Methods Europe (Copenhagen, Denmark, 22-Jul-2002 - 24-Jul-2002)

Lecture Notes in Computer Science (LNCS), 2391, Springer Verlag

2002

DOI: https://doi.org/10.1007/3-540-45614-7_2

Files and links (1)

url

https://doi.org/10.1007/3-540-45614-7_2View

Published Version

Abstract

Computer Software

specification-based testing

boundary values

set constraint solving

B method

Z notation

We present a method for black-box boundary testing from B and Z formal specifications. The basis of the method is to test every operation of the system at every boundary state using all input boundary values of that operation. The test generation process is highly automated. It starts by calculating boundary goals from Pre/Post predicates derived from the formal model. Then each boundary goal is instantiated to a reachable boundary state, by searching for a sequence of operations that reaches the boundary goal from the initial state. This process makes intensive use of a set-oriented constraint technology, both for boundary computation and to traverse the state space. The method was designed on the basis of industrial applications in the domain of critical software (Smart card and transportation). Application results show the effectiveness and the scalability of the method. In this paper, we give an overview of the method and focus on the calculation of the boundary goals and states.

Details

Title: Automated boundary testing from Z and B
Authors: Bruno Legeard (Author) - Université de Franche-Comté, France
Fabien Peureux (Author) - Université de Franche-Comté, France
Mark Utting (Author) - Université de Franche-Comté, France
Contributors: Lars-Henrik Eriksson (Editor)
Peter Lindsay (Editor)
Publication details: Formal Methods Europe 2002: Getting IT Right, pp.21-40
Conference details: International Symposium of Formal Methods Europe (Copenhagen, Denmark, 22-Jul-2002 - 24-Jul-2002)
Series: Lecture Notes in Computer Science (LNCS); 2391
Publisher: Springer Verlag
DOI: 10.1007/3-540-45614-7_2
ISBN: 9783540439288
Organisation Unit: University of the Sunshine Coast, Queensland; School of Science and Engineering - Legacy
Language: English
Record Identifier: 99449810802621
Output Type: Book chapter

Metrics

544 Record Views