5.2 Category of Methods "Design Verification" (DVER)


		Annex 1
		5.2 Design Verification

DVER - Designverifikation

Contents
5.2.1 Overview

5.2.1.1 Appraisal Criteria
5.2.1.2 Individual Methods
5.2.1.3 Comparison of the individual Methods

5.2.2 Individual Descriptions

5.2.2.1 Classical Design Verification
5.2.2.2 Verification during Development (Design Verification)
5.2.2.3 Formal Transformation (Design)

5.2.1 Overview

A "formal verification" is a verification done with formal, i. e. mathematically correct means. A "verification" is an evaluation in order to prove a product of a development activity with regard to the fulfillment of the requirements generated within preceding activities. If the product is considered a specification for which a formal verification is to be carried out then the process is called Design Verification. The time of the proof shows the difference between the individual methods.

5.2.1.1 Appraisal Criteria

The following contains a list of criteria helping to select individual methods:

existence of an informal detailed specification (in this case often it is easier first to generate a formal specification and later to verify),
existence of a formal detailed specification,
separation of the refinement steps and the assessment (e. g. if the verification shall take place within the scope of QA),
availability of tools.

5.2.1.2 Individual Methods

According to the time of proof the Design Verification can be differentiated in

These methods are presented in the following individual descriptions. In order to make it easier to distinguish between the individual methods these methods are first compared with each other.

5.2.1.3 Comparison of the individual Methods

The objective of the individual DVER methods is identical. They only differ concerning the time at which the proof of correctness is performed. Within the Classical Design Verification this is done only after completing the refined specification. Within Verification during Development every refinement step is proved immediately. within the Formal Transformation a specification is transformed into a target specification by means of transformation rules. Prior to the transformation the correctness of the transformation rules is already mathematically proven.

The Classical Design Verification is to favor those cases where a refined informal specification already exists, because then it is not necessary to trace the development steps again. Within this method often it is difficult to localize or to correct an error especially in those cases when it is not possible to furnish the proof of the refinement or when it turns out that it is no refinement. Within the Formal Transformation and the Verification during Development every development step is proved immediately. Therefore, an error is easy to correct, but it may be difficult to comprehend again the design decisions of an already existing informal specification. The proof tasks within the Formal Transformation are the slightest because of the proofs having generally been proved already. On the other hand, it is difficult to provide a complete set of transformation rules necessary for the refinement step.

Classical Design Verification Verification during Development (Design Verification) Formal Transformation (Design)
Great effort for the proof Great effort for the proof Comparatively small effort for the proof, because the rules have already been proven but the development may require a long time
Easy to achieve consistency relating to the informal specification already in existence Comparatively difficult to achieve consistency relating to the informal specification already in existence Difficult to achieve consistency relating to the informal specification already in existence
Set of rules generally sufficient Set of rules generally sufficient Set of rules generally only sufficient for limited problems
Possible to test the specification prior to the proof Not possible to test the specification before Not possible to test the specification before
Later verification possible Later verification not possible Later verification not possible
Error detection possibly difficult; possibly work has to be started again Error detection simple, because every design step is immediately proven; possibly only the last step has to be modified In practice errors not possible, because only correct transformations are performed

Classical Design Verification	Verification during Development (Design Verification)	Formal Transformation (Design)
Great effort for the proof	Great effort for the proof	Comparatively small effort for the proof, because the rules have already been proven but the development may require a long time
Easy to achieve consistency relating to the informal specification already in existence	Comparatively difficult to achieve consistency relating to the informal specification already in existence	Difficult to achieve consistency relating to the informal specification already in existence
Set of rules generally sufficient	Set of rules generally sufficient	Set of rules generally only sufficient for limited problems
Possible to test the specification prior to the proof	Not possible to test the specification before	Not possible to test the specification before
Later verification possible	Later verification not possible	Later verification not possible
Error detection possibly difficult; possibly work has to be started again	Error detection simple, because every design step is immediately proven; possibly only the last step has to be modified	In practice errors not possible, because only correct transformations are performed

Table 5.2: DVER: Differences between Individual Methods

5.2.2 Individual Descriptions
5.2.2.1 Classical Design Verification
5.2.2.2 Verification during Development
5.2.2.3 Formal Transformation

GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster


Contents		5.2.1 Overview	5.2.1.1 Appraisal Criteria 5.2.1.2 Individual Methods 5.2.1.3 Comparison of the individual Methods
		5.2.2 Individual Descriptions	5.2.2.1 Classical Design Verification 5.2.2.2 Verification during Development (Design Verification) 5.2.2.3 Formal Transformation (Design)