Previous Next Methods Allocation  
Annex 1  
5.3.2.4 Specification by Traces  

  Spezifikation mittels Traces

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

    /Hoare, 1985/

    2 Brief Characteristic of the Method

    The Specification of Traces is a formal specification describing the sequences of a program, i. e. the order of individual states or individual operations. The specification is done via the characteristics of these traces.

    3 Application of the Method in the V-Model

    The Specification of Traces may be applied for the description of the operation behavior on every level of abstraction. This specification also is ideal for the description of sequences of combined programs or automata (e. g. parallelism).

    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