Validation-Driven Development

TL;DR

This paper introduces a validation-driven development process that emphasizes validating requirements specifications in formal development, utilizing problem frames and validation obligations, demonstrated through an aviation case study.

Contribution

It proposes a novel validation-driven development process based on problem frames and validation obligations, shifting focus from verification to validation in formal methods.

Findings

Effective validation process demonstrated in aviation case study

Prioritizing validation improves requirement correctness assurance

Process integrates validation into formal development steps

Abstract

Formal methods play a fundamental role in asserting the correctness of requirements specifications. However, historically, formal method experts have primarily focused on verifying those specifications. Although equally important, validation of requirements specifications often takes the back seat. This paper introduces a validation-driven development (VDD) process that prioritizes validating requirements in formal development. The VDD process is built upon problem frames - a requirements analysis approach - and validation obligations (VOs) - the concept of breaking down the overall validation of a specification and linking it to refinement steps. The effectiveness of the VDD process is demonstrated through a case study in the aviation industry.