Previous Next Methods Allocation  
Annex 1  
4.8 Interface DVER-FS  

  • 1 Characterization of the Interface
  • 2 Example
  • 3 Tool Support
  • 4 Literature
  • 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
    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

    Previous Next GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster