|4.19 Method Category "Formal Specification" (FS)|
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).
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:
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:
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.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.
|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.
|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.
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.
|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.
|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|
|GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster|