Previous Next Methods Allocation  
Annex 1  
5.3.2.5 Specification by Temporal Logic  

  Spezifikation mittels temporaler Logik

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

    /Kroeger, 1987/ chap. 4

    2 Brief Characteristic of the Method

    The Specification by Temporal Logic is a formal specification describing the program via temporal logic. Temporal logic concerns with statements being dependent of the time. Using temporal logic statements about certain program states can be made but also about the program sequence. Every state corresponds to a discrete moment.

    3 Application of the Method in the V-Model

    The Specification by Temporal Logic may be applied for the description of the operation behavior on every level of abstraction.

    This specification also is ideal for the description of timing connections of programs.

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

    Previous Next Last Updated 01.Jan.2002