Previous Next Methods Allocation  
Annex 1 Verification during Development (Program Verification)  

  Verification during Development (Program)

  • 1 Identification/Definition of the Method
  • 2 Brief Characteristic of the Method
  • 3 Application of the Method in the V-Model
  • 4 Interfaces
  • 5 Further Information
  • 6 Literature
  • 1 Identification/Definition of the Method

    /Brix, 1986/

    2 Brief Characteristic of the Method

    By Verification during Development a specification is refined step by step into an executable code.

    Prior to the next design step every design step is proved. After the last design step the program is available.

    3 Application of the Method in the V-Model

    Within the V-Model the Verification during Development can be applied for the self assessment in SD. This method may only be allocated to SD because the team having refined the specification down to an executable code should perform the proof.

    4 Interfaces

    There is an interface to FS - Formal Specification. The Verification during Development has to be suited to the formal specification language and the programming language.

    5 Further Information

    - not applicable -

    6 Literature

    /Baader, 1990/ Basic features of formal methods as a stock-taking of tools and concepts
    /Brix, 1986/ By means of the examples CARTESIANA, a verification tool from Siemens, the basic features of "Program Verification during Development" are explained
    /Kersten, 1990/ Several reports on "formal specification and verification"
    /Kröger, 1987/ Deals with temporal logic and verification of statements in temporal logic
    /Loeckx, 1987/ Describes the mathematical background of several formal verification methods (e. g. Floyd Method, Axiomatic Method of Hoare, Fixed-point Induction), as shown by some examples. Furthermore the problems of correctness and completeness are discussed.

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