 |
 |
 |
|
| Annex 1 | |||
| 5.3.2.5 Specification by Temporal Logic |
Spezifikation mittels temporaler Logik
 Contents
|
|
|---|
1 Identification/Definition of the Method
/Kroeger, 1987/ chap. 4
2 Brief Characteristic of the Method
The Specification by Temporal Logic is a formal specification describing the program via temporal logic. Temporal logic concerns with statements being dependent of the time. Using temporal logic statements about certain program states can be made but also about the program sequence. Every state corresponds to a discrete moment.
3 Application of the Method in the V-Model
The Specification by Temporal Logic may be applied for the description of the operation behavior on every level of abstraction.
This specification also is ideal for the description of timing connections of programs.
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, 90/ | Basic features of formal methods as a stock-taking of tools and concepts |
|---|---|
| /Björner, 90/ | Manual of the conference VDM '90; main emphasis is put on actual topics with regard to the formal specification languages VDM and Z |
| /Gehani, 86/ | Several specification topics, principles and characteristics for a good specification, several specification methods, the application of formal specification techniques in practice are discussed |
| /Hayes, 87/ | Specification in Z |
| /Jones, 90/ | Describes VDM and its basis |
| /Kersten, 90/ | Several reports on "formal specification and verification" |
| /Kroeger, 1987/ | Deals with temporal logic and verification of statements in temporal logic |
|
|
|
Last Updated 01.Jan.2002 |