 |
 |
 |
|
| Annex 1 | |||
| 5.4.2.1 Classical Program Verification |
Klassische Programmverifikation
 Contents
|
|
|---|
1 Identification/Definition of the Method
/Baader, 1990/ sections II and III of chapter 2.1
2 Brief Characteristic of the Method
The Classical Program Verification proves a program to be a correct implementation of a specification. The proof is only done after the completion of the program.
3 Application of the Method in the V-Model
Within the V-Model the Classical Design Verification can be applied for the self assessment in SD. It is not sensible to allocate this method to QA because the team having generated the program should perform the proof.
4 Interfaces
There is an interface to FS - Formal Specification. The Classical Program Verification has to be suited to the formal specification language and the implementation 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, 87/ | 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. |
|
|
|
GDPA Online
Last Updated 01.Jan.2002
Updated by Webmaster
Last Revised 01.Jan.2002
Revised by Webmaster
|