Taxonomy/1. Quality/08. Verification and validation

How can we convince ourselves and others that an artefact is adequate?

As explained under Rationality, when we do not →believe that something is the case, theoretically there are three ways to convince ouselves and others: insight, induction, and deduction. The questions that relate reality to a formula should be answered by inductive methods (experiments) or, in the easiest case, by insight. The question that relates a blueprint to a specification can be answered by deduction: by proving a Correctness Theorem. At least when a specification an blueprint is known.

blueprint	4. Does every every artefact with this structure have the described properties?	Specification
5. Does the artefact have the structure defined by the blueprint?	3. Does the artefact have the specified properties?	2. Are the right properties specified?
artefact	1. Is the artefact adequate?	properties in physical reality

We will investigate these questions one by one, both for the case when specification and blueprint are known or not. But first of all we must clarify some confusion.

A remark on terminology

There are two fundamentally different kinds of questions. But beware! In computer science they traditionally have confusing names:

Does physical reality conform to a formula?

This is the question about the truth (Latin: "veritas") of the formula. Computer scientiests call the activity to establish truth validation (from Latin "validus": "legally sound" / "logically correct" / "derived conforming to the rules").

Is a formula related to another one?

This is the question whether a valid (i.e. formally correct) mathematical proof exists that connects the two formulae. For the special case "Does a blueprint satisfy a specification?" computer scientiests call the activity to find and check such a formal proof verification, from "verify" ("to establish to be true, as by evidence").

Canonical activities

Validation of a specification

Does a given specification specify the right properties? There are two cases.

1. The specified artefact is part of a bigger system, and its specification stems from a correctness theorem at the next higher level. In this case the answer is "yes" due to that correctness theorem.
2. There is no correctness theorem at the next higher level. In this case there are three possibilities.
   1. Insight. The specification is so clear and self-understanding that we say: "yes, this is what we want".
   2. Simulation or prototyping. We construct an artefact in such a way that we are sure it is an implementation of the specification and observe it and experiment with it. This can be done by moenas of "rapid prototyping" or by simulation. This approach is mainly inductive.
   3. Reasoning. We can transform the specification, hoping this leads to insight. We can try to prove properties that should also hold when the intended properties hold. We can try to check whether our specification is compatible with the specifications of other parts of the surrounding artefact. This approach is mainly deductive.

Validation of an implementation

Is an existing artefact an implementation of the specification? If that question cannot be anwered by ensuring that it is a correct realisation of a blueprint that satisfies the specification (either because we do not find a proof for the correctness theorem or because it is physically impossible to see whether the artefact has the intended structure), we can hope to gain some evidence by testing, an inductive approach. Testing theory investigates how to do this systematically, making use of the knowledge contained in the blueprint. The basic assumption is that even if we cannot check whether the artefact is a correct realisation of the blueprint, by contruction its structure will at least be similar to the one defined by the blueprint.

Verification of a design

Does a given blueprint satisfy a given specification? To be sure we have to prove the corresponding Correctness Theorem and to check whether this proof contains no flaws.

Finding a proof can be very difficult, even undecidable. But during rational Development the information necessary for a proof comes along. Therefore it is a good idea to develop the proof together with the blueprint like in Monotonic and Non-Monotonic Refinement. The blueprint is then correct by construction.

Specifications can be very large, usually because they are a conjunction of many different requirements. These can, of course, be proved one by one. If the specification that cannot be broken down in this way is so detailed that a proof will be too complex for the existing proof methods and tools, one might consider to go for a less ambitious goal and focus on important, but simple properties. (One might, for example, prove that a system of programs is deadlock-free and simply believe that, as long as there are no deadlocks, it will do the right things.)

Even if we are interested in the verification of very simple properties only, the blueprint can be much too large to be handled by tools. This is the case when the code of large programs is used as a ^∞X blueprint. (Remember the millennium problem, where the blueprint was completely available n the form of all Cobol and assembly programs in all computers of the network of the company.) It would have been better to have developed the program in a modular way conform to the Chinese Box Principle, each box accompanied by a ⁷X blueprint. An unstructured blueprint at the level of program code or screws and nuts is so large that it is nearly useless.

Nearly, but not quite. It could be used to simulate the artefact. The behaviour of some artefacts can be simulated in less time than the real artefact would consume. In any case, failures of simulated artefacts will be less dangerous than failures of the real ting. If a proof cannot be found, the blueprint can still be used for experiments–an inductive approach.

Validation of a realisation

Is a given artefact a realisation of a given blueprint? It is, if the right parts are assembled correctly.

1. The parts are the right ones if they are implementations of the parts' specifications in the blueprint.
2. Whether they are assembled correctly, can be ensured in two ways.
   1. Inspection.
   2. Correctness by construction. The artefact has been realised by a quality production process that ensures correctness.

Ideal rational verification and validation

In an ideal situation,

• designer and customer have agreed on a specification,
• the designer has produced a decomposition of an artefact into a small numer of well-specified components in terms of a ⁷X blueprint,
• some provider has provided these parts and evidence that they are adequate,
• the parts have been assembled conform the blueprint.

A Correctness Theorem consists of a →blueprint, a →specification, and possibly some Domain knowledge that was not built into the blueprint and specification languages used. As specification and a blueprint are given, verification means proving the theorem. Validation means ensuring that the theorem is really about the artefact and properties under discussion.

Verification and validation in realistic situations

400px

Here a more realistic situation.

• An artefact is given in the form of a plant or vehicle containing a controller and a control program.
• There is no complete blueprint, only the code of the program in some cryptic language and some diagrams about the machinery.
• There is a fairly clear idea about the overall purpose, but that idea has not been formalised.
• There are domain experts, but they do not share a common language and canot read formal specifications and blueprints.
• There is a feeling that the control program could be improved for better performance of the plant.
• The owner of the plant or the authorities want to know whether the whole thing functions correctly.

The idea to convert this situation into an ideal one is not attractive. We would have to formalise all known requirements and to write the other half of the blueprint by analysing all bouts and pipes in the plant and their underling connections–only to end up with something far too big to be handled even by the most modern supercomputers.

Nevertheless we can let ourselves be guided by a good understanding of this unreachable ideal and do some useful verification and validation: instead of going for the full blueprint we can try to derive a "light version" that contains just enough information about the artefact that verification an validation of some essential properties with today's theories and tools becomes feasible.

Vital properties instead of all requirements

As mentioned above, instead of verifying and validating the full adequacy, i.e. instead of using a specification which states all requirements, we can treat properties one by one. And we can decide to ensure simpler properties. Let S be a specification stating such a simple property.

Decomposition

The control program is a ^∞X blueprint. If we would decompose the machinery without expert knowledge, we would arrive at another ^∞X blueprint. We dismissed this as infeasible. The other extreme would we a blueprint of two parts, namely the controller and the rest of the machinery. It is unlikely, however, to arrive at a correct specification of the given machinery whithout decomposing it. Therefore we recommend to consult Domain experts of the solution domain and look for a decomposition of the plant or vehicle into a small number of meaningful parts.

Necessary assumptions

If we wanted to build the artefact, we would need a blueprint that gives the full specifications of these parts. But we only want to prove that certain properties hold. We do not need to include more in a part's specification than needed for the proof. It is a question of leaving knowledge away that is not needed to establish S. Instead of using full specifications we work with the necessary assumptions only. Let us call them s₁, ... , s_n.

Control: the missing link

Let N be the necessary domain knowledge. If a controller is needed to ensure S, the specification of the controller must be the X in the correctness theorem:

N∧s1∧ ... ∧sn∧X⇒S

Instead of proving if the control program together with the machinery is adequate, we thus first derive a control specification X. The proof that the actual controller satisfies X can then be done at the next lower level, without knowledge about the machinery–a simple application of the Chinese Box Principle.

Verification models

Obviously,

s1∧ ... ∧sn∧X

is the "light version" of the blueprint we wanted to find. We will call it a verification model (for the artefact under discussion) with respect to S. A useful verification model must...

• of course be a formal model of the artefact, in other words: the artefact should be a correct realisation of it;
• be so simple and clear that it can be discussed witth experts, in other words, it should be understandable;
• be so small that it can be useful for formal verification.

Methodology around verification models is treated here:

• Modelling in the contexts of verification and design
• Modelling
• Non-Monotonic Refinement