4.32 Method Cathegory "Program Verification" (PVER)

  4.32 Methodenkategorie "Programmverifikation" (PVER)

Contents		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

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

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:

• When performing the Classical Program Verification the proof is started when the code of the unit to be verified is generated. Generally for each statement of the specification either the "strongest" postcondition when starting at the precondition or the "weakest" precondition when starting at the postcondition is searched.
• When performing the Verification during Development (Program Verification) a statement of the specification is immediately verified just after being coded. Corresponding to the "Classical Program Verification" the strongest postcondition or the weakest precondition is searched.
• The Formal Transformation (Program) is a conversion of the specification by means of predefined rules and is a proof that the conditions are fulfilled under which the rules are valid. It has to be evaluated that the transformation rules lead only to correct program constructs.

3 Limits of the Methods Application

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

5 Interfaces

6 Further Literature

7 Functional Tool Requirements

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