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.