Previous Next Methods Allocation  
Annex 1 Mathematical Specification  

  Mathematische Spezifikation

  • 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/ section II, chap. 1.2 (here: "operational specification")

    2 Brief Characteristic of the Method

    The Mathematical Specification is a formal specification defining the behavior of operations by the description of pre- and postconditions.

    The postcondition describes the states that are allowed to be reached after the execution of the operation if the precondition was valid before the execution of the operation.

    3 Application of the Method in the V-Model

    The Mathematical Specification may be applied for the description of operations on every level of abstraction.

    4 Interfaces

    There are interfaces to DVER - Design Verification, PVER - Program Verification and ACC - Analysis of Covert Channels.

    5 Further Information

    - not applicable -

    6 Literature

    /Baader, 1990/ Basic features of formal methods as a stock-taking of tools and concepts
    /Björner, 1990/ Manual of the conference VDM '90; main emphasis is put on actual topics with regard to the formal specification languages VDM and Z
    /Gehani, 1986/ Several specification topics, principles and characteristics for a good specification, several specification methods, the application of formal specification techniques in practice are discussed
    /Hayes, 1987/ Specification in Z
    /Jones, 1990/ Describes VDM and its basis
    /Kersten, 1990/ Several reports on "formal specification and verification"
    /Kröger, 1987/ Deals with temporal logic and verification of statements in temporal logic

    Previous Next Last Updated 01.Jan.2002