B model animation for external verification

The B method is a model-based approach covering all the software development process, from the specification to the code. External verification of B models aims to determine whether they correctly capture the informal requirements. It is argued that verification techniques like B model animation or code testing should accompany the formal development process and give a feedback of the system that is actually being specified. A uniform testing framework, irrespective of whether the input cases are executed on the final code or on the formal models, is presented. A B development process is considered as a series of stages where concrete models are built gradually based on the more abstract ones, the final code being just a compiled version of the most concrete model. A definition of test correctness, related to the one of refinement, is introduced. The consequences in terms of required animation facilities are discussed