Synthesis of scenario based test cases from B models

Abstract

When models are formal, model based testing approaches usually construct a coverage graph through symbolic execution and derive test cases in the form of paths in the coverage graph. Thereafter consistency between the model and the implementation is verified in relation to the test cases. Existing approaches, especially when dealing with model oriented languages like B, partition the input space of each operation in the model to create operation instances, and then animate the model in relation to these instances. The paths or the test cases are now a sequence of operation instances. However, in this approach, there is no guarantee that we test the user scenarios. In this paper, we first define scenario based test cases in relation to the initial specification. When this specification passes through a succession of refinements, we derive scenario based test cases for each refinement and show that all these test cases are equivalent to the test cases of the original specification. © 2006 Springer-Verlag Berlin/Heidelberg.