Previous Next Methods Allocation  
Annex 1 Formal Transformation (Program)  

  Formale Transformation (Program)

  • 1 Identification/Definition of the Method
  • 2 Brief Characteristic of the Method
  • 3 Application of the Method in the V-Model
  • 4 Interfaces
  • 5 Further Information
  • 6 Literature
  • 1 Identification/Definition of the Method

    /Baader, 1990/ sections II and III of chapter 2.4

    2 Brief Characteristic of the Method

    According to predefined, mathematically proven transformation rules the Formal Transformation converts a specification until the required result is achieved. If the transformation rules are only valid under certain conditions then it has to be proven that it is allowed to apply the transformation rule.

    Since the transformation rules are proven to be correct the result also is correct.

    3 Application of the Method in the V-Model

    Since the development and the proof should be done together this method has to be allocated to SD.

    4 Interfaces

    There is an interface to FS - Formal Specification. The Formal Transformation has to be suitable to the formal specification language and the programming 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, 1987/ 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.

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