Lessons from DEPLOYment

TL;DR

This paper discusses lessons learned from Bosch's DEPLOY project, emphasizing that no single formalism suffices for all development phases and that formal methods should be applied selectively where most appropriate.

Contribution

It highlights the limitations of using a single formalism like Event-B across all development stages and advocates for targeted application of formal methods.

Findings

Single formalism cannot cover all development phases.

Formal methods should be used selectively based on suitability.

No universal solution exists for all lifecycle stages.

Abstract

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.