Model-Based Specification

Modelsexplicit or mentalplay a big role in failure analysis and in test design. This technique is a style of modeling aptly named model-based specification: it relies on building a simple model of the data and/or state of the thing being specified, then operations (e.g., steps in a use case) are defined in terms of how they modify that model.

There is a subtle but very important point that needs to be made about the state variables used in model-based specification, especially if you are accustomed to "instance variables" or "member variables" in object-oriented programming languages. The variables WidgetsInStock and WidgetsInStock' are two separate variables in the model we are building. They do refer to the same single instance/member variable in the application (assuming that is how the application was implemented), but it requires multiple, separate variables in the model-based specification itself in order to be able to talk about the different states the application instance/member variable might be in.