Pragmatic Use of B: The Power of Formal Methods without the Bulk
Christophe Métayer, François Bustany, Mathieu Clabaut · 2014
The aim of this chapter is to show that practices widely used in classic developments can also be applied in the context of formal processes, facilitating their implementation and acceptability. In the context of modern industry, it is rare to find development projects for systems, equipment or software which do not include the creation of one or more prototypes in the earliest stages. The chapter provides some elements of response to these issues concerning the relationships and responsibilities of the development and validation teams. B is known and used in relation to safety requirements. The B method for software can be used to improve practices based on event-B, and vice-versa. The use of formal methods such as B allows engineers to focus on their primary role in specifying and designing systems or programs, using powerful reasoning tools, without needing to devote time and effort to later, purely coding-related stages.