|4.10 Category of Methods "Design Verification" (DVER)|
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.
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.
There are three different procedures to do the formal Design Verification (DVER):
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.
|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.2 - Design of Internal and External SW Interfaces, DVER could assist in the generation of Interface Description.Description of the Interfaces.
|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.
|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|
|GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster|