Biomedical Engineering Reference
In-Depth Information
event has a firing condition (a guard) as opposed to a pre-condition. It may fire when
its guard is true. Event based models have proved useful in requirement analysis,
modelling distributed systems and in the discovery/design of both distributed and
sequential programming algorithms.
After an extensive experience with B, current work by Abrial is proposing the for-
mulation of a second version of the method [
3
]. This distills experience gained with
the event-based approach and provides a general framework for the development of
discrete systems
. Although this widens the scope of the method, the mathematical
foundations of both versions of the method are the same.
3.1.2 Proof-Based Development
Proof-based development methods [
2
,
7
,
34
] integrate formal proof techniques in
the development of software systems. The main idea is to start with a very abstract
model of the system under development. Details are gradually added to this first
model by building a sequence of more concrete ones. The relationship between two
successive models in this sequence is that of
refinement
[
2
,
7
,
9
,
19
]. The essence
of the refinement relationship is that it preserves already proved
system properties
including safety properties and termination.
A development gives rise to a number of, so-called,
proof obligations
, which
guarantee its correctness. Such proof obligations are discharged by the proof tool
using automatic and interactive proof procedures supported by a proof engine [
21
,
22
].
At the most abstract level it is obligatory to describe the static properties of a
model's data by means of an
invariant
predicate. This gives rise to proof obligations
relating to the consistency of the model. They are required to ensure that data prop-
erties which are claimed to be invariant are preserved by the events or operations of
the model. Each refinement step is associated with a further invariant which relates
the data of the more concrete model to that of the abstract model and states any
additional invariant properties of the (possibly richer) concrete data model. These
invariants, so-called
gluing invariants
are used in the formulation of the refinement
proof obligations.
The goal of a B development is to obtain a
proved model
. Since the development
process leads to numerous proof obligations, the mastering of proof complexity is a
crucial issue. Even if a proof tool is available, its effective power is limited by clas-
sical results over logical theories and we must distribute the complexity of proofs
over the components of the current development, e.g. by refinement. Refinement
has the potential to decrease the complexity of the proof process whilst allowing for
traceability of requirements.
B models rarely need to make assumptions about the
size
of a system being mod-
elled, e.g. the number of nodes in a network. This is in contrast to model checking
approaches [
20
]. The price to pay is to face possibly complex mathematical theories
Search WWH ::
Custom Search