Information Technology Reference
In-Depth Information
target
(
s
3
)=
{
}
1
futures
(
s
3
)=
∅
futures
(
s
3
)=
means that there is no state from which the property state
machine can reach the final state via the execution after line 3. According to the
preceding two conditions,
s
3
is a “nop shadow” that can be removed.
∅
1 public static void m(String args[]) {
2 Connection c1 = new Connection(args[0]);
…………………
0 {}
3 c1.close();
…………………
1 {}
4 c1.reconnect ();
…………………
0
reconnect, write
close
write
write
close
0
1
2
reconnect
close
{1, 2}
5
c1.write(args[1]);
…………………
0 {2}
reconnect
“ConnectionClosed” typestate property
6}
Fig. 1.
An example for Nop-shadows Analysis
After removing a “nop shadow”, the
source
(
st
)and
futures
(
st
) of each state-
ment will be calculated again, until no “nop shadow” exists. If there is no shadow
after NSA, the program is proved to satisfy the typestate property. For exam-
ple, all the shadows of the program in Figure 1 will be removed finally. For the
inter-procedural cases, the method calls are soundly approximated by using the
transitive closure of the shadows in the called methods.
3 Motivating Examples
We motivate our optimizations of NSA through two examples. We also use the
“ConnectionClosed” property in Figure 1 as the typestate property. Figure 2
shows an example that invokes the “close” and “write” methods of the class
Connection. The shadows at line 7 and 10 violate the typestate property, because
they can both drive the state machine into the final state. The “close” operation
at line 8 is between these two violating shadows. Hence, from the semantics of
the program and the property FSM (
c.f.
Figure 1), the runtime monitor does
not need to monitor the shadow at line 8. Whereas, the original NSA cannot
identify the shadow at line 8 as a “nop shadow” at compile-time. The reason is
explained as follows.
For the sake of brevity, Figure 2 only shows partial critical state information
calculated by the forward and backward analysis. In order to distinguish the
typestates of multiple different objects or groups of related objects, the data-
flow analysis of NSA propagates “configurations” instead of only state sets [7].
A configuration specifies the state information of some specific objects. A con-
figuration
C
=(
Q,b
) is composed by a state set
Q
and a variable binding
b
.
