 |
 |
 |
|
| Annex 1 | |||
| 5.3.2.2 Axiomatic Specification (Algebraic Specification) |
Axiomatische Spezifikation (Algebraische Spezifikation)
 Contents
|
|
|---|
1 Identification/Definition of the Method
/Baader, 1990/ section II, chap. 1.2
2 Brief Characteristic of the Method
The Axiomatic Specification is a formal specification defining the semantics of functions of objects by a description of the relations between different objects and functions. The description is made by axioms (predicate-logical formula).
The Algebraic Specification describes functions in the form of an algebra. An algebra consists of a signature and the axioms. The signature consists of a family of object sets (carrier sets) and a number of operations in this carrier set with their functionality. The axioms describe the characteristics of this operations by means of algebraic equations.
3 Application of the Method in the V-Model
The Axiomatic Specification may be applied for the description of operations on every level of abstraction. In particular, it is suitable for the first phases (e. g. also for the formal security model).
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, 1990/ | Basic features of formal methods as a stock-taking of tools and concepts |
|---|---|
| /Björner, 1990/ | Manual of the conference VDM '90; main emphasis is put on actual topics with regard to the formal specification languages VDM and Z |
| /Gehani, 1986/ | Several specification topics, principles and characteristics for a good specification, several specification methods, the application of formal specification techniques in practice are discussed |
| /Hayes, 1987/ | Specification in Z |
| /Jones, 1990/ | Describes VDM and its basis |
| /Kersten, 1990/ | Several reports on "formal specification and verification" |
| /Kröger, 1987/ | Deals with temporal logic and verification of statements in temporal logic |
|
|
|
Last Updated 01.Jan.2002 |