Information Technology Reference
In-Depth Information
The alphabet contains four types of events: LOCK, UNLOCK, PROT (representing an
access to a protected field) and UNPROT (representing an access to an unprotected
field). The states of the monitor have the following interpretation:
s
1
- initial state,
s
2
-lockisheld,
s
3
- lock is not held,
s
4
- error state (i.e., violation of locking discipline
has been detected).
In general, after a gap, the joint probability distribution
P
(
X
t
,S
t
) may contain non-
zero probabilities for all composite states, reflecting uncertainty in the current state of
the DFA. The monitor can, however, quickly peek at the state of the lock to check
whether it is held by the associated thread. If so, the DFA can only be in states
s
2
or
s
4
, so probabilities of composite states containing
s
1
or
s
3
can be set to zero. If not,
the DFA can only be in states
s
1
,
s
3
,or
s
4
, so the probabilities of composite states
containing
s
2
can be set to zero. For example, some sample entries in the probability
distribution for peek events are
P
(
s
2
|
notHeld) = 0.
Figure 4 shows in a graphical way the transition and observation probability distri-
butions of an HMM model of a system that usually follows this locking discipline but
has a small chance of violating it.
held) = 1 and
P
(
s
2
|
5
RVPF Algorithm
This section describes our R
UNTIME
V
ERIFICATION
P
ARTICLE
F
ILTERING
(RVPF) al-
gorithm, which performs approximate state estimation based on particle filtering. Like
the original RVSE algorithm [10], RVPF estimates the probability that the system is
in a composite state (
x
t
,s
t
) at time
t
.Let(
x
(
i
t
,s
(
i
t
) denote the state, also called the
“position”, of the
i
'th particle at time
t
.
5.1
The Precomputation Phase
In Line 1 of the RVPF algorithm, whose pseudo code is given on page 157, the prob-
abilities
P
(
O
t
|
X
t−
1
,O
t
) are precomputed so they can be accessed
quickly by the rest of the algorithm. The exact details of the precomputation are shown
in algorithm P
RECOMPUTE
P
ROBABILITIES
.
X
t−
1
) and
P
(
X
t
|
Algorithm
P
RECOMPUTE
P
ROBABILITIES
Input
: System Model HMM
H
=(
X,O,P
(
X
t
| X
t−
1
)
, P
(
O
t
| X
t
)
, P
(
X
0
))
Output
:
P
(
O
t
| X
t−
1
)
, P
(
X
t
| X
t−
1
,O
t
)
1
P
(
O
t
| X
t−
1
) =
P
(
X
t
| X
t−
1
)
P
(
O
t
| X
t
)
2
for
i
= 1
to
|
dom(
X
)
|
do
3
for
j
= 1
to
|
dom(
X
)
|
do
for
k
= 1
to
|
dom(
O
)
|
do
4
5
P
(
X
t
=
x
i
| X
t−
1
=
x
j
,O
t
=
o
k
) =
P
(
X
t
=
x
i
| X
t−
1
=
x
j
)
· P
(
O
t
=
o
k
| X
t
=
x
i
)
/ P
(
O
t
=
o
k
| X
t−
1
=
x
j
)
6
end
7
end
8
end
9
return
[
P
(
O
t
| X
t−
1
)
, P
(
X
t
| X
t−
1
,O
t
)]
