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.

翻译：形式化方法在确保需求规格正确性方面发挥着基础性作用。然而，历史上形式化方法专家主要专注于验证这些规格。尽管同样重要，但需求规格的验证常常被置于次要地位。本文介绍了一种验证驱动开发（VDD）流程，该流程优先在形式化开发中验证需求。VDD流程基于问题框架（一种需求分析方法）和验证义务（VOs）（即分解规格的整体验证并将其与精化步骤相关联的概念）。通过航空工业中的案例研究，证明了VDD流程的有效性。