验证义务：一种检查需求与其形式化规约一致性的新方法

传统上，从业者主要将形式化方法用于质量保证过程的一半：验证（我们是否正确地构建了软件？）。另一半——确认（我们是否构建了正确的软件？）——受到的关注相对较少。虽然验证是基于精化的形式化方法的核心，其中每个新的精化步骤必须保留其抽象模型的所有性质，但确认通常推迟到开发的最晚阶段，此时模型可被自动执行。因此需求和需求解释中的错误被发现得太晚：通常在开发过程结束时。在本文中，我们提出一种新方法，在开发的较早阶段检查需求与其基于精化的形式化规约之间的一致性。我们提出的方法——“验证义务”——基于一个简单的理念：验证和确认都是系统所有精化步骤的组成部分。