Information Technology Reference
In-Depth Information
model checking abstractions of the full AVI and/or FML layers against reference
processes satisfying the properties. Instead, the abstraction principles were ap-
plied to smaller sub-systems { for example to each of the process sub-systems
shown in Figure 1 { in order to prove a modied local verication goal. The
new goals dened for the sub-systems were elaborated in such a way that the
original correctness requirements could be deduced from the new goals by com-
positional reasoning over the parallel combination of sub-systems. To increase
the eciency of the compositional reasoning process, it was tried to identify
whether sub-systems could be regarded as (renements of) instances of generic
process classes with known compositional properties.
Example 2.
In the compositional reasoning process performed to prove dead-
lock freedom of the FML, it could be shown by model checking that each of
the process sub-systems depicted in Figure 1 is a renement of a process of
type \multiplexer/concentrator" specied as
MUXCON
below. The denition
of
MUXCON
is generic in the number
N
specifying how many outputs must
be produced before the next input can be accepted and the number, names and
alphabet of input channels
.
Observe that an instance of
MUXCON
dened with
N
= 0 never refuses an
input.
f
in
1
;:::;
in
n
g
and output channels
f
out
1
;:::;
out
m
g
MUXCON
[
N
; f
in
1
;:::;
in
n
g; f
out
1
;:::;
out
m
g
]=
MC
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
](0)
MC
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
](
n
)=
if
(
n
=0)
then
(
GET
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
]
(
STOP
u
PUT
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
](1)))
else
PUT
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
](
n
)
GET
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
]=
(
e
:
fj
in
1
;:::;
in
`
jg
e
!
MC
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
](
N
))
PUT
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
](
n
)=
(
u
e
:
fj
out
1
;:::;
out
m
jg
e
!
MC
[
N
; f
in
1
;:::;
in
`
g; f
out
1
;:::;
out
m
g
](
n
−
1))
The following generic theory is associated with the above process class:
Theorem 1.
A network of process instances P
1
;:::;
P
q
from class
MUXCON
[
N
; f
in
1
;:::;
in
n
g; f
out
1
;:::;
out
m
g
]
is free of deadlocks, if every com-
munication cycle
c
j
1
−!
c
j
2
−! :::
c
j
k
−
1
−!
c
j
k
−!
P
j
1
P
j
2
P
j
k
P
j
1
contains at least one process instance P
j
`
denedwithN
=0
.
t
Search WWH ::
Custom Search