Making the most of formal specification throughAnimation, Testing and Proof.

Abstract The use of formality in software development enables formal manipulation at thesymbolic level and hence can yield new perspectives on the design which can be submitted to inspection and interactive or automatic analysis. We describe the experience of anindustrial pilot project which undertook a formal development using VDM and B and employed a number of techniques for the analysis of the formal texts by animation, testcase generation and proof. We assess the effectiveness of methodology and techniques adopted by measuring the introduction and detection of faults