Information Technology Reference
In-Depth Information
In summary, we expect the abstract and concrete systems to be related as
depicted below:
a
Signal
O
a
=
O
c
O
a
=
O
c
O
a
=
O
c
c
C
4.2
Proving Renement by Simulation plus Abstraction Mapping
V
C
;
C
;
C
;O
c
) be a given abstract and
concrete systems. The standard way of proving that
V
A
;
A
;
A
;O
a
)and
Let
A
=(
C
=(
C
renes
A
(cf. [1]) is based
on the identication of an
abstraction mapping
V
C
) mapping concrete
states to abstract states, and establishing the premises of rule
V
A
=
(
ref
presented
in Fig. 4. In many places, the mapping
is referred to as
renement mapping
.
Premise R1 of the rule ensures that the mapping
maps every initial concrete
For an abstraction mapping
V
A
=
(
V
C
),
R1.
C
^ V
A
=
(
V
C
)
!
A
Initiation
R2.
V
A
=
(
V
C
)
^
C
^ V
A
=
(
V
C
)
!
A
Propagation
R3.
V
A
=
(
V
C
)
!O
a
=
O
c
Compatibility with observations
C v A
Fig. 4.
Rule
ref
.
state into an initial abstract state. Premise R2 requires that if the abstract state
s
A
s
0
C
and the concrete state
s
C
are
-related, and
is a
C
-successor of
s
C
,
s
0
A
=
s
0
C
)isa
then the abstract state
s
A
. Together, R1 and
R2 establish by induction that, for every concrete computation
(
A
-successor of
0
1
C
:
s
C
;s
C
;:::;
0
1
there exists a corresponding abstract computation
A
:
s
A
;s
A
;:::;
such that
j
A
j
C
s
=
(
s
) for every
j
=0
;
1
;:::
. Applying premise R3, we obtain that the
observations obtained from
A
and
C
are equal. This shows that rule
ref
is
sound.
Rule
, in the form presented in Fig. 4, is often not complete. In many
cases we need to add an auxiliary invariant to the premises. However, in the case
at hand, the relation
ref
V
A
=
(
V
C
) is the only invariant we need.
4.3
Construction of the Mapping
To complete the description of our verication methodology, it only remains to
describe how we can construct automatically the abstraction mapping
.
The range of the mapping
is a tuple of values over the domains of the
abstract variables
V
A
. In fact, for every abstract variable
v 2 V
A
, the mapping
Search WWH ::
Custom Search