Formal methods into practice: case studies in the application of the B method

Abstract

The paper reports on an investigation into the application of the B method of formal software development. Six case studies are described, each exploring a different aspect of the use of the B methodology and toolkit. The case studies are drawn from a diverse range of applications and address different aspects of the software development lifecycle. The notation, method and tool support are assessed and conclusions are drawn concerning the use of B and formal methods generally.