Formal Engineering Methods, International Conference on (1998)
Dec. 9, 1998 to Dec. 11, 1998
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
S. Behnia and H. Waeselynck, "B Model Animation for External Verification," Formal Engineering Methods, International Conference on(ICFEM), Brisbane, Australia, 1998, pp. 36.