4.19 Method Category "Formal Specification" (FS)

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

• 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

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
Design
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/
Module/
Database
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

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