These allow the logical properties
of a computer system to be predicted from a model of the system using logic to calculate if a system
description:
??? Is internally consistent
??? Has certain properties
??? Has a correctly-interpreted requirements specification
Systematic checking of these calculations may be automated using such languages as Z and VDM.
Formal modeling of a system usually entails translating a system description from a non-mathematical
model (dataflow diagrams, object diagrams, scenarios, UML, English text, etc.) into a formal specification,
using one of several formal languages. FM tools can then be employed to evaluate this specification to check
its completeness and consistency.
FM techniques and tools can be applied to the specification and verification of products from each
development life-cycle: requirement, high- and low-level design, and implementation.
Formal methods force users and developers to use a common language in requiring and designing
systems. The baselines against which system tests are defined remain as essential as before but by using
a formal language essential relationships can be defined and proven. See Figure 4.9.
See section A.11 to get a sense of how a system test can be developed from a formal specification.
The dangers of using a formal specification are:
??? Staff and users may claim they cannot understand it.
??? The use of the formal specification may be subverted by inconsistencies with the natural language
specification.
Pages:
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180