Previous Next Methods Allocation  
4.19 Method Category "Formal Specification" (FS)  

  4.19 Methodenkategorie "Formale Spezifikation" (FS)

  • 1 Identification/Definition of the Method
  • 2 Brief Characteristic of the Method
  • 3 Limits of the Methods Application
  • 4 Specification of the Methods Allocation
  • 5 Interfaces
  • 6 Further Literature
  • 7 Functional Tool Requirements
  • 1 Identification/Definition of the Method

    FS is a category of methods; the individual applicable methods are described in more detail FS - Formal Specification (in Annex 1) to the Methods Allocation by listing the selection criteria. A special methods is only defined within the scope of the operationalization.

    A formal specification is a specification written in a formal notation. This notation is based on well-founded mathematical concepts. These concepts were used to define the syntax and semantics of the notation and the proof rules which support logical reasoning. It must be possible to derive formal specifications from the set of axioms. It must be possible to prove the validity of characteristics like the generation of a valid statement (compare /ITSEC BSI/, 2.76).

    2 Brief Characteristic of the Method

    Objective and Purpose

    A formal specification represents a formal model of a part of the system. Generally, this model may be implemented in different ways. The amount of possible implementations is restricted by hierarchical refinement, e. g. by stating valid states of the system more precisely or by inserting interim states.

    A formal specification is necessary for the description of the formal model.

    Input information for FS is a non-formal requirements description or a non-formal design and-if available-a formal specification of the activity preceding the refinement.

    Means of Representation

    Means of representation for FS is a formal notation based on a calculus of formal logic. Which kind of calculus is most suitable depends on the sort of requirements to be proved. The most important classes of formal specifications are:

    Operational Sequence

    Details about the functions and the required features of the product to be implemented in non formal means of representation are the starting point for the formal specification. Valid states, state transitions, invariants and/or pre- and postconditions of the individual operations are specified and derived from the functional requirements and the derived sequences. Ideally all but generally only a part of the requirements may be formally represented.

    This formal specification is further refined. The formal specification of the preceding level of refinement and the refined non-formal specification are the basis for the refinement. Seen in general, the refinement of a specification follows the schema presented below:

    Figure FS.1
    Figure FS.1: Refinement of Formal Specifications

    If the internal consistency of a design shall be proved by the specification then one specification level may be sufficient. Otherwise the formal specification may be refined down to a programming specification when going through several levels of refinement. A transition to another specification method is only sensible if the methods applied for the specifications are compatible.

    3 Limits of the Methods Application

    The generation and assessment of formal specifications requires a sound mathematical knowledge of the developer and of QA. Syntax check and static semantics check should be supported by tools.

    A specific education is essential for the understanding and the further developing of formal specifications (e. g. education for programmers).

    The mathematical, the axiomatic and the algorithmic specification are the ones most applied. Different aspects of a design may be represented by different formal specification methods. Seen from the state of the art, hierarchical refinements should be performed within a specification method because a transition to another method generally leads to interface problems and makes the formal verification more difficult.

    By observing these limitations, the IT system development has an enormous chance, however, to generate first rate, high-quality IT systems when applying the formal methods.

    4 Specification of the Methods Allocation

    No. Activity Description
    4.1 SD2.5
    Interface Description
    By means of the formal specifications in the System Architecture critical interfaces are selected and are specified precisely and completely.

    This representation supplements the informal Interface Description.Description of the interfaces.

    4.2 SD4.1
    SW Architecture
    Within this activity the cooperation of the processes is expressed by FS. If there was not generated a formal model in activity SD2.2 - Realization of Efficiency Analysis then SD4.1 - SW Architecture Design is a suitable entry point to formalize the requirements.

    Method FS also expresses and formally defines the interrelation of the SW components, SW modules and databases in subproducts SW Architecture.Individual Descriptions, SW Architecture.Dynamic Sequence Model.

    This representation supplements the non-formal Preliminary Design.

    4.3 SD4.2
    Design of Internal and
    External SW Interfaces
    By means of the formal specifications in the SW Architecture critical interfaces are selected and are specified precisely and completely.

    This representation supplements the informal Interface Description.Description of the Interfaces.

    4.4 SD5.1
    Description of
    SW Component/
    This representation is a hierarchical refinement of the specification form SD4.1 - SW Architecture Design and it takes into consideration the results of the non-formal design refinement.

    This representation supplements the non-formal Detailed Design.

    FS could assist in the generation of SW Design (Module).SW Component/SW Module Description, Data Dictionary.Data Description and Data Dictionary.Data Realization.

    5 Interfaces

    No. Interface Observation Information in Annex 1
    5.1 FS-DVER The Design Verification (DVER - Design Verification) requires a Formal Specification (FS). 4.8 Interface DVER-FS
    5.2 FS-PVER The Program Verification (PVER - Program Verification) requires a Formal Specification (FS). 4.13 Interface FS-PVER
    5.3 FS-ACC The ACC - Analysis of Covert Channels requires a Formal Specification (FS) if the analysis shall be done formally.
    4.1 Interface ACC-FS

    6 Literature

    /Baader, 1990/ Methoden zur formalen Spezifikation und Verifikation von Software
    /Björner, 1990/ VDM '90: VDM and Z. Formal Methods in Software Development
    /Gehani, 1986/ Software Specification Techniques
    /Hayes, 1987/ Specification Case Studies
    /Jones, 1990/ Systematic Software Development using VDM
    /Kersten, 1990/ Sichere Software (Formale Spezifikation und Verifikation vertrauenswürdiger Systeme)
    /Kröger, 1987/ Temporal Logic of Programs

    7 Functional Tool Requirements

    SSD29 - Formal Specification

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