 |
 |
 |
|
| Annex 1 | |||
| 4.8 Interface DVER-FS |
 Contents
|
|
|---|
1 Characterization of the Interface
The interface corresponds to the type "information transmission in sequential order"The category of methods DVER - Design Verification serves as the proof that a specification is a refinement of another specification. Input for DVER therefore is a formal specification possibly on two different levels depending on the selected individual DVER method (this is so for the Classical Design Verification and the Verification during Development (Design Verification)). Depending on the selected individual DVER method the result again is a formal specification (this is so for the Formal Transformation (Design)) or an assessment result.
Therefore FS - Formal Specification is applied for the description of the system, DVER, on the other hand, is applied for the proof that these descriptions are consistent.
2 Example
The following figure explains the connections between specifications on two different levels of abstraction:
Figure 4.10: Means for Generating a Correct Refinement
Cf. example in FS-PVER.
3 Tool Support
Because of the complexity of DVER tool support is absolutely necessary. The evaluation (respectively the applied rules) has to be adjusted to the selected specification language.
4 Literature
| /Brock, 1990/ | Handbook for the formal specification language RAISE, a further development of the formal specification language VDM extended by the possibility of algebraic specification and by parallelism |
| /Jones, 1990/ | describes VDM and its basis |
| /Kersten, 1990/ | several reports to "formal specification and verification" |
| /Nicholls, 90/ | articles on the Z User Workshop 1989, mainly concerning Z |
|
|
|
GDPA Online
Last Updated 01.Jan.2002
Updated by Webmaster
Last Revised 01.Jan.2002
Revised by Webmaster
|