Lessons from DEPLOYment
This addresses the problem of over-reliance on formal methods in software engineering, but it is incremental as it builds on existing critiques.
The paper reviews lessons from two pilot projects in the DEPLOY project, finding that no single formalism like Event-B can provide a complete solution from requirements to code, and that formalisms should be used only where suitable rather than forced across the entire lifecycle.
This paper reviews the major lessons learnt during two significant pilot projects by Bosch Research during the DEPLOY project. Principally, the use of a single formalism, even when it comes together with a rigorous refinement methodology like Event-B, cannot offer a complete solution. Unfortunately (but not unexpectedly), we cannot offer a panacea to cover every phase from requirements to code; in fact any specific formalism or language (or tool) should be used only where and when it is really suitable and not necessarily (and somehow forcibly) over the entire lifecycle.