Formalism of Requirements for Safety-Critical Software: Where Does the Benefit Come From?

TL;DR

This paper investigates whether formalising safety-critical software requirements actually reduces errors, proposing an experiment to test the causal relationship and explore various explanations for potential benefits.

Contribution

It introduces a structured experiment to empirically evaluate the benefits of formalising requirements, addressing a hypothesis lacking strong causal evidence.

Findings

Multiple explanations for benefits of formalisation are identified.

An experiment design is proposed to test these explanations.

The causal link between formalisation and error reduction remains to be empirically validated.

Abstract

Safety and assurance standards often rely on the principle that requirements errors can be minimised by expressing the requirements more formally. Although numerous case studies have shown that the act of formalising previously informal requirements finds requirements errors, this principle is really just a hypothesis. An industrially persuasive causal relationship between formalisation and better requirements has yet to be established. We describe multiple competing explanations for this hypothesis, in terms of the levels of precision, re-formulation, expertise, effort and automation that are typically associated with formalising requirements. We then propose an experiment to distinguish between these explanations, without necessarily excluding the possibility that none of them are correct.