Information Technology Reference
In-Depth Information
justify that our optimizations are effective in the majority of cases. Section 6
describes the related work and the paper is concluded in Section 7.
2 Nop-shadows Analysis
As in the literature [6,7,17], we also use the term “shadow” to represent an
instrumentation point created for runtime monitoring. NSA is a static typestate
analysis method proposed and implemented in the Clara framework [6], which
extends tracematch [2] with static analysis to remove “nop shadows”. Here a
“nop shadow” means that the shadow does not influence the results of runtime
monitoring,
i.e.
, it can neither trigger nor suppress a property violation [6,7].
Clara consists of three static analysis stages, in which NSA is the most expen-
sive and precise one. Given a typestate property (usually a finite-state machine
(FSM)) and an instrumented Java program, NSA uses an intra-procedural data-
flow analysis to check whether a shadow in a method of the program can be
removed. The basic idea of NSA is to compute the reachable states of each
statement in a program according to the semantics of the program and the mon-
itored typestate property. Given an FSM typestate property
M
and its state set
S
, for each statement
st
, there are two types of reachable states:
source
(
st
)and
futures
(
st
), which are calculated respectively by a
forward
data-flow analysis
(forward analysis) and a
backward
data-flow analysis (backward analysis). The
source set
source
(
st
)
S
contains all the states that can be reached before ex-
ecuting
st
from the beginning of the program;
futures
(
st
)
⊆
(
S
)isthe
future
set, and each element of
futures
(
st
) contains the states from which the remain-
der program execution after
st
can reach a final state (usually the error state) of
M
. Therefore, for a given shadow
s
, which is usually a method call statement in
the program, NSA identifies
s
as a “nop shadow” if the execution of the shadow
has no impact on the monitoring result, which can be formalized by following
two conditions:
-
target
(
s
)
⊆
P
}
is the resulting state set after executing
s
,
δ
(
q
1
,s
) is the resulting state after
executing
s
from the state
q
1
according to the FSM property
M
,and
F
is
the final state set of
M
. This condition means the execution of
s
does not
directly lead to an error state.
∩
F
=
∅
,where
target
(
s
)=
{
q
2
|∃
q
1
∈
sources
(
s
)
•
q
2
=
δ
(
q
1
,s
)
-
∀
Q
.Itmeansthe
execution of
s
does not influence whether or not a final state will be reached.
q
1
∈
source
(
s
)
,
∀
Q
∈
futures
(
s
)
•
q
1
∈
Q
⇔
δ
(
q
1
,s
)
∈
The shadow
s
can be removed if both conditions are valid.
Figure 1 gives an example for NSA. The left part is an FSM for “Connec-
tionClosed” [7] typestate property, which requires the “write” operation should
not be called after a connection is closed. The right part displays a program
annotated with the state information of each statement. The elements in the
source
set and the
futures
set of each statement are next to the downward and
upward arrows, respectively. For instance, for the shadow
s
3
atline3,wehave:
source
(
s
3
)=
{
0
}
