4.10 Category of Methods "Design Verification" (DVER)

#### 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):

• When performing the Classical Design Verification the proof is started after the refinmenet of the starting specification is completed.
• When performing the Verification during Development (Design Verification) each refinement step of a statement of the starting specification is verified immediately.
• The Formal Transformation (Design) is a concersion of the starting specification by means of predefined rules and is a proof that the conditions are fulfilled under which the rules are valid. It has to be evaluated that the transformation rules are correct according to the utilized logical calculus.

#### 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
,
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

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