Previous Next Methods Allocation  
4.32 Method Cathegory "Program Verification" (PVER)  

  4.32 Methodenkategorie "Programmverifikation" (PVER)

  • 1 Identification/Definition of the Method
  • 2 Brief Characteristic of the Method
  • 3 Limits of the Methods Application
  • 4 Specification of the Methods Allocation
  • 5 Interfaces
  • 6 Further Literature
  • 7 Functional Tool Requirements
  • 1 Identification/Definition of the Method

    Method Program Verification (PVER) is a category of methods; the individual applicable formal verification procedures are described in more detail in PVER - Program Verification (in Annex 1) by listing the selection criteria. A special methods is only defined within the scope of the operationalization.

    Within the Program Verification it is proved by means of formal logic that a program is a refinement of a specification and that all requirements to this higher-level specification are met too.

    2 Brief Characteristic of the Method

    Objective and Purpose

    The objective of PVER is to mathematically exactly prove that the program code is a correct implementation of the specification.

    Means of Representation

    On the part of the specification the means of representation described at FS - Formal Specification are applied. On the part of the program a programming language is used. The semantics of the programming language has to be formally defined. Further rules have to be described for the proof steps (e. g. Hoare Calculus).

    Operational Sequence

    There are three different procedures to do the formal Program Verification, such as to do the formal DVER - Design Verification:

    3 Limits of the Methods Application

    Often the used programming languages are too extensive and too inaccurate for being able to define the semantics of every construct by formal rules. For several constructs of today's languages there are no rules known. This fact implies a limitation of the number of used programming language constructs in order to be able to perform PVER.

    In generally, fully automatic Program Verification is not possible. The verification conditions should be generated automatically. But often, automatically generated verification conditions are very long and therefore are difficult to prove by hand. Tool support therefore is strongly required.

    Performing Program Verification requires a sound mathematical education. For those parts of the proof not fully automated (e. g. finding the invariant) much experience is necessary. The program either should be written by the team that shall perform the proof or at least should be written in a form supporting the verification (e. g. invariant recorded in form of comments).

    By observing these limitations the IT system development has an enormous chance to generate first rate, high-quality IT systems, however, by applying the formal methods.

    4 Specification of the Methods Allocation

    No. Activity Description
    4.1 SD6.1
    Coding of SW Modules

    Realization of Database

    Self-Assesment of the
    SW Module/Database

    The correspondence of the program code to the formal specification used as programming specification is evaluated.

    5 Interfaces

    No. Interface Observation Information in Annex 1
    5.1 PVER-FS PVER requires a calculus which describes the semantics of the programming language by means of a specification language (FS). 4.13 Interface FS-PVER

    6 Further Literature

    /Baader, 1990/ Methoden zur formalen Spezifikation und Verifikation von Software
    /Brix, 1986/ Rechnergestützte Programmkonstruktion und -verifikation mit formalen Regeln
    /Kersten, 1990/ Sichere Software (Formale Spezifikation und Verifikation vertrauenswürdiger Systeme)
    /Kröger, 1987/ Temporal Logic of Programs
    /Loeckx, 1987/ The Foundation of Program Verification

    7 Functional Tool Requirements

    SSD30 - Formal Verification

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