16.3. Checking Requirements with Verification Cases

A verification case can have as its objective the verification of one or more requirements on a subject — meaning the requirements are asserted to be true if the subject passes whatever sort of testing is being modeled. The subject of the verification case is automatically bound to the subject of the verified requirements.

A verification case defines a process (as a sequence of actions) for verifying whether a subject satisfies one or more requirements.

The result of a verification case is a verdict on whether the subject of the case satisfies the requirements:

1. Pass indicates that the subject satisfies the requirements.
2. Fail indicates that the subject does not satisfy the requirements.
3. Inconclusive indicates that a determination could not be made.
4. Error indicates that an error occurred during the performance of the verification.

These four possible outcomes have been coded in the predefined enumeration VerificationCases::VerdictKind.

A typical verification case includes a set of verification actions such as:

1. Collect data about the subject as needed to support the verification objective (e.g., through analysis, inspection, demonstration, and test).
2. Analyze the collected data, e.g., determine the probability distribution, mean, and standard deviation.
3. Evaluate the results of the analysis based on the objective to produce a verdict.

An example verification case definition is the following:

verification def VehicleMassTest {
  import VerificationCases::VerdictKind;
  import VerificationCases::PassIf;
  subject testVehicle : Vehicle;
  objective vehicleMassVerificationObjective {
    verify testVehicle.massRequirement;
  }
  action collectData {
    in part testVehicle : Vehicle = VehicleMassTest::testVehicle;
    out massMeasured :> ISQ::mass;
  }
  action processData {
    in massMeasured :> ISQ::mass = collectData.massMeasured;
    out massProcessed :> ISQ::mass;
  }
  action evaluateData {
    in massProcessed :> ISQ::mass = processData.massProcessed;
    out verdict : VerdictKind =
      PassIf( testVehicle.massRequirement( vehicle = testVehicle,
                                      massActual = massProcessed));
  }
  return verdict : VerdictKind = evaluateData.verdict;
}

Notice that the predefined enumeration VerdictKind and the predefined function PassIf are imported from the library package VerificationCases.