Application and benefits of formal methods in software development

TLDR

Formal methods attract research interest yet remain uncommon in industry because their integration into the software life‑cycle is poorly understood. The study defines “using a formal method” and investigates the application and benefits of VDM within the DoD‑STD‑2167A development model. The authors analyze each DoD‑STD‑2167A activity for VDM suitability and potential benefits. The analysis yields a comprehensive view of how formal methods can be employed throughout the software process.

Abstract

Formal methods for software development receive much attention in research centres, but are rarely used in industry for the development of (large) software systems. One of the reasons is that little is known about the integration of formal methods in the software process, and the exact role of formal methods in the software life-cycle is still unclear. In this paper, a detailed examination is made of the application of, and the benefits resulting from, a generally applicable formal method (VDM) in a standard model for software development (DoD-STD-2167A). Currently, there is no general agreement on how formal methods should be used, but in order to analyse the use of formal methods in the software process, a clear view of such use is essential. Therefore, we show what is meant by ‘using a formal method’. The different activities of DoD-STD-2167A are analysed with regard to their suitability for applying VDM and the benefits that may result from applying VDM for that activity. Based on this analysis, an overall view on the usage of formal methods in the software process is formulated.