4.19 Method Category "Formal Specification" (FS)

  4.19 Methodenkategorie "Formale Spezifikation" (FS)

Contents		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

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

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:

• Mathematical Specification: It describes states and state transitions by means of the pre- and postconditions of an operation. (Area of application is the description of terminating programs or procedures)
• Axiomatic Specification (Algebraic Specification): It defines the semantics of functions and objects as predicate-logical axioms. (Suitable for security models and for the description of abstract data types)
• Algorithmic Specification: It describes the operation behavior by means of a computation rule on a low level of abstraction. (Area of application is the software design; the algorithmic specification is used as a programming specification)
• Specification by Traces: It represents the time sequence of states or operations (trace) and their characteristics. (Suitable for the description of concurrent processes or automata)
• Specification by Temporal Logic: Discrete instants are represented as states. (Suitable for statements about the sequence of operations)

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: 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

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

5 Interfaces

6 Literature

7 Functional Tool Requirements

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