Formalism of Requirements for Safety-Critical Software: Where Does the Benefit Come From?
This addresses the need for empirical validation in safety-critical software development, but is incremental as it builds on existing case studies without presenting new results.
The paper tackles the problem of establishing a causal link between formalizing requirements and reducing errors in safety-critical software, proposing an experiment to test competing explanations for observed benefits.
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.