Previous Next Methods Allocation  
Annex 1  
5.4 Category of Methods "Program Verification" (PVER)  

  PVER - Programmverifikation

Contents  
  • 5.4.1 Overview
  • 5.4.1.1 Appraisal Criteria
  • 5.4.1.2 Individual Methods
  • 5.4.1.3 Comparison of the individual Methods
  •     
      
  • 5.4.2 Individual Descriptions
  • 5.4.2.1 Classical Program Verification
  • 5.4.2.2 Verification during Development (Program Verification)
  • 5.4.2.3 Formal Transformation (Program)
  • 5.4.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 a program for which the formal verification is performed, then the process is called Program Verification. The methods are different-analog to Design Verification-in the timing of the proof activities.

    5.4.1.1 Appraisal Criteria

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

    5.4.1.2 Individual Methods

    According to the time of proof the Program Verification can be differentiated in
    1. Classical Program Verification,
    2. Verification during Development (Program Verification) and
    3. Formal Transformation (Program)

    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.4.1.3 Comparison of the individual Methods

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

    The Classical Program Verification the program may already be tested before it is proved. 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 correctness or when it turns out that it is not a correct program. Within the Formal Transformation (Program) and the Verification during Development (Program Verification) every development step is proved immediately. Therefore, an error is easy to correct, but it may be difficult to optimize the program. The proof tasks within the Formal Transformation (Program) are the most insubstantial because the proofs generally have been proved already. On the other hand, it is difficult to provide a complete set of transformation rules necessary for the implementation.

    Classical Program Verification Verification during Development (Program Verification) Formal Transformation (Program)
    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
    Set of rules generally sufficient for limited programming constructs Set of rules generally sufficient for limited programming constructs Set of rules generally only sufficient for limited problems
    Error detection possibly difficult; possibly work has to be started again Error detection simple, because every design step is proved immediately; possibly only the last step has to be modified In practice errors not possible, because only correct transformations are performed
    Later verification possible Later verification not possible Later verification not possible
    Testing the program is possible prior to proof Testing the program is not possible until the proof is nearly completed Program is not available until the last transformation

    Table 5.4: PVER: Differences between Individual Methods

    5.4.2 Individual Descriptions

    5.4.2.1 Classical Program Verification
    5.4.2.2 Verification during Development (Program Verification)
    5.4.2.3 Formal Transformation (Program)

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