 |
 |
 |
|
| Annex 1 | |||
| 5.3.2.4 Specification by Traces |
Spezifikation mittels Traces
 Contents
|
|
|---|
1 Identification/Definition of the Method
/Hoare, 1985/
2 Brief Characteristic of the Method
The Specification of Traces is a formal specification describing the sequences of a program, i. e. the order of individual states or individual operations. The specification is done via the characteristics of these traces.
3 Application of the Method in the V-Model
The Specification of Traces may be applied for the description of the operation behavior on every level of abstraction. This specification also is ideal for the description of sequences of combined programs or automata (e. g. parallelism).
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 |