|4.32 Method Cathegory "Program Verification" (PVER)|
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.
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).
There are three different procedures to do the formal Program Verification, such as to do the formal DVER - Design Verification:
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.
Coding of SW Modules,
|The correspondence of the program code to the formal specification used as programming specification is evaluated.
|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|
|GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster|