Information Technology Reference
In-Depth Information
regardless of their positions in the syntactic description of
M
n
. The synchro-
nization predicate
is then a set of multisets of actions. Each multiset describes
a possible combination of labels on component transitions that make up a tran-
sition of the parameterized system. For instance, if the pair
f
send
;
receive
g
is
in
, but neither of send nor receive is in any other set of the synchronization
predicate, then each occurrence of a send must be synchronized with a matching
receive. In order to be able to model broadcast and global synchronizations, we
allow one of the actions in a synchronization to have the special superscript
!
,
receive
!
meaning \all other processes". For instance, the set
f
send
;
g
denotes a
broadcast by one process to all other processes.
The above requirements on synchronization concern a system
M
n
, which is
closed
in the sense that it does not interact with its environment. Later, in Section 3.2,
we will consider
open
systems which represent a part of some
M
n
which can syn-
chronize with other components. Synchronizations of an open system need only
contain a subset of the labels of some multiset of the synchronization predicate.
Two open systems may synchronize, and the labels on transitions are formed as
the union of labels of the synchronizing systems in the natural way. Continuing
the above example where
f
send
;
receive
g
is in
, a transition of an open system
may be labeled by send only.
We could also have considered parameterized systems with a linearly ordered
topology, in which components are arranged in an order, as shown in the syntac-
tic description of
M
n
. The synchronization predicate will then be a set of
strings
of labels.
Correctness Properties
We will only consider linear-time safety properties of pa-
rameterized systems, which can be stated as a requirement on the executions of
the controller, and a
bounded
arbitrary set of distinct components. Such proper-
ties can be transformed into invariants of the form
8i
1
;:::;i
k
:
alldi
(
i
1
;:::;i
k
)=
)
(
i
1
;:::;i
k
)
where
is a predicate on the local states of the controller and the compo-
nents with indices
i
1
;:::;i
k
) states that all indices
i
1
;:::;i
k
are distinct. We shall call such a formula a
universal assertion.
As an
example, we can specify mutual exclusion by the invariant
i
1
;:::;i
k
, and where
alldi
(
8i 6
=
j: :
(
critical
[
i
]
^ critical
[
j
])
Examples of correctness properties that can be expressed in this form are: mutual
exclusion, clock synchronization, security properties, etc.
The checking of an invariant can be equivalently reformulated as a reachability
property. For instance, the above invariant means that it is not possible to reach
a state which satises the negation
9i 6
=
j:
(
critical
[
i
]
^ critical
[
j
]) of the above
invariant. We shall call such a formula an
existential assertion
Search WWH ::
Custom Search