Previous Next Methods Allocation  
Annex 1  
5.2.2.3 Formal Transformation (Design)  

  Formale Transformation (Design)

Contents  
  • 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 suited to the formal specification language.

    5 Further Information

    - not applicable -

    6 Literature

    /Baader, 1990/ Basic features of formal methods as a stock-taking of tools and concepts
    /Brock, 1990/ Handbook for the formal specification language RAISE, a further development of the formal specification language VDM extended by the possibility of algebraic specification and b parallelism
    /Jones, 1990/ Describes VDM and its basis
    /Kersten, 1990/ Several reports on "formal specification and verification"
    /Nicholls, 1990/ Articles on the Z User workshop 1989, mainly concerning Z

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