Biomedical Engineering Reference
In-Depth Information
not normally describe lowest level software, such as mathematical subroutine pack-
ages or data structure manipulation, but will describe the response of the system
to events and inputs, to a degree, necessary to establish the critical properties. For
instance, in a cardiac pacemaker the sensor and actuator are functioning correctly.
This specification reflects the primary user requirements derived through successive
evolutions, each of which transforms an abstract specification to become more con-
crete. Evolution steps may involve the usual notion of formal refinement, and may
also involve introducing additional constraints required in the final solution. Hence,
a specification during the evolution process is considered to provide the functional
constraints on the final concrete specification rather than a complete description.
4.3.3 Formal Verification
This phase has a very important role in the formal development. To demonstrate
that the informal requirements satisfy the safety properties of interest, the infor-
mal requirements and the properties are passed to a theorem prover and then prover
is applied to prove formally that the informal requirements satisfy the properties.
A formal notation can be analysed and manipulated using mathematical operators,
mathematical proof procedures can be used to test (and prove) the internal consis-
tency (including data conservation) and syntactic correctness of the specifications.
Furthermore, the completeness of the specification can be checked in the sense that
all enumerated options and elements have been specified. However, no specifica-
tion language can ensure completeness in the sense that all the user's requirements
have been met, because of the informal human-intention nature of the requirements
specifications [ 38 ]. Finally, the implementation of the system will be in a formal
language (i.e., the programming language), it is easier to avoid misconceptions and
ambiguities in crossing the divide from formal specifications to formal implemen-
tations. A formal verification phase is done to ensure that,
The model is designed correctly
The algorithms have been implemented properly
The model does not contain errors, oversights, or bugs
In summary, we can say that verification ensures that the specification is complete
and that mistakes have not been made in implementing the model. But verification
does not ensure the model,
Solves an important problem
Meets a specified set of model requirements
Correctly reflects the working of a real world process
In Fig. 4.1 , this phase provides a feedback to the formalisation phase in case of
not satisfying given properties of the system. The feedback approach is allowed to
modify the formal model and verify again it through the formal verification phase.
The verification process is applied to continue until not to find the correct formal
model according to the expected behaviour of the system.
Search WWH ::




Custom Search