Previous Next Methods Allocation  
4.10 Category of Methods "Design Verification" (DVER)  

  4.10 Methodenkategorie "Designverifikation" (DVER)

Contents  
  • 1 Identification/Definition of the Method
  • 2 Brief Characteristic of the Method
  • 3 Limits of the Methods Application
  • 4 Specification of the Methods Allocation
  • 5 Interfaces
  • 6 Further Literature
  • 7 Functional Tool Requirements

    • 1 Identification/Definition of the Method

    Design Verification (DVER) is a category of methods; the individual applicable methods (formal verification procedures) are described in more detail in DVER - Design Verification (in Annex 1) by listing the selection criteria. A special method is only defined within the scope of the operationalization.

    Within the Design Verification it is proced bay means of formal logic that a formal specification (detailed specification) is a refinement of a starting specification and that all requirements to the starting specification are met too.

    2 Brief Characteristic of the Method

    Objective and Purpose

    A specification is refined by going into details an by stating more precisely the statements and conditions. It is the objective of the Design Verification to mathematically prove that the refined specification further is meeting the statements of the starting specification.

    The Design Verification is necessary for proving the formal security model.

    Means of Representation

    The means of representation correspond to those of the Formal Specification. Furthermore rules for the proof steps have to be given.

    Operational Sequence

    There are three different procedures to do the formal Design Verification (DVER):

    3 Limits of the Methods Application

    Not always it is possible to prove all required characteristics of a specification (e. g. completeness, termination).

    In general, fully automatic Design Verification is not possible. The verification conditions should be generated automatically. But often, automatically generated verification conditions are very long and therefore are difficult to prove by hand. Design Verification withour tools therefore is error-prone.

    Performing Design Verification requires a sound mathematical education. For those parts of the proof not fully automated much experience is necessary. The refinement either should be done by the team that shall perform the proof or at least should be done in a form supporting the verification.

    By observing these limitations, IT system development only gets the enormous chance to generate first rate, high-quality IT systems if formal methods are applied.

    4 Specification of the Methods Allocation

    No. Activity Description
    4.1 SD2.5
    Interface Description    ,

    SD4.1
    SW Architecture Design    ,

    SD4.2
    Design of
    Internal and External
    SW Interfaces

    		 If a formal specification was generated in the preceding activities (e. g. activity SD2.2 - Realization of Efficiency Analysis) it is verified that the formal specification (e. g. of interfaces or SW Architecture) generated in this activity corresponds with the specification (e. g. formal security model of activity SD2.2 - Realization of Efficiency Analysis). If further improvements are formally realized in the activity it is verified that they are consistent.

    In activity SD2.5 - Interface Description, DVER could assist in the generation of Interface Description.Description of the interfaces.

    In activity SD4.1 - SW Architecture Design, DVER could assist in the generation of SW Architecture.Individual Descriptions and SW Architecture.Dynamic Sequence Model.

    In activity SD4.2 - Design of Internal and External SW Interfaces, DVER could assist in the generation of Interface Description.Description of the Interfaces.

    4.2 SD5.1
    Description of
    SW Component/
    Module/
    Database    		 The correspondence of the formal specification of the detailed design and the SW Architecture is verified and, if further refinements are performed, the correctness of them is proved also.

    DVER could assist in the generation of SW Design (Module).SW Component/SW Module Description, Data Dictionary.Data Description and Data Dictionary.Data Realization.

    5 Interfaces

    No. Interface Observation Information in Annex 1
    5.1 DVER-FS DVER requires a formally specified detailed specification for to be verified and a formally specified starting specification. These specifications should be written in the same specification language. 4.8 Interface DVER-FS

    6 Literature

    /Brock, 1990/ RAISE METHOD
    /Jones, 1990/ Systematic Software Development using VDM
    /Kersten, 1990/ Sichere Software (Formale Spezifikation und Verifikation vertrauenswürdiger Systeme)
    /Nicholls, 1990/ Z User Workshop

    7 Functional Tool Requirements

    SSD30 - Formal Verification

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