4.32 Method Cathegory "Program Verification" (PVER)

#### 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:

• 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

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
,
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

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