Preliminary analysis cycle for B-method software development

The main benefit of using formal specifications early in the software life-cycle is to allow a priori errors detection. More precisely, incompleteness and inconsistency deficiencies can be detected very early and confidence resulting from correctness proofs increases. Thus, formal methods fit into the Verification and Validation activities, relieving but not replacing Software Testing. In the present state of the art, many tools and techniques for formal methods are fairly strong on formal aspects, but weak on methodological aspects. Likewise, there is a lack of support for the testing process. Within the framework of our case study we give guidelines to construct formal specifications, especially for B-method. In this paper we describe our method to develop a formal specification and show how the produced documents could be inputs to the testing process