Databases Reference
In-Depth Information
end1
b
a
start
aCalled
c
end2
FIGURE 5.5: A property FSM where end1 and end2 are final states.
a
1
,
a
2
, a
3
, … , a
k
e
x
start
end
a
1
Called
FIGURE
5.6:
Trigger
FSM
that
accepts
the
regular
language
e(a
1
+ a
2
+ ::: + a
k
)
x.
Hence PDMC restricts the form of B and T by modeling B to be a regu-
lar language accepted byF(B = L(F)), and T as a context-free language
accepted by a PDAP(of program P). In general, we have TL(P), which
then implies T\BL(F)\L(P). Consequently, if L(F)\L(P) is empty, T\B
is denitely empty. However, if L(F)\L(P) is not empty, T\B could either
be empty or not. Since L(F) is a regular language and L(P) is a context-free
language, L(F)\L(P) can be captured by a PDA, say P, and hence the nal
state ofFis reached if and only if the PDA P accepts the empty language.
There are ecient algorithms to determine if the language accepted by the
PDA is empty [35]. Once P is constructed, PDMC checks to see if any final
configuration is reachable in P. Chen and Wagner [20] use the preceding anal-
ysis to adapt PDMC for lightweight property checking. We use the preceding
analysis for static trace generation. We call the FSMs such as the one used in
Figure 5.6 as Triggers. By using Triggers, we have achieved two purposes:
We have produced T
ex
, the set of traces (in the program) that begin
with e and end with x instead of T
0
T.
The knowledge of A = fa
1
;a
2
;a
3
;:::;a
k
g allows us to extract A(t) from
any t2T
ex
.
Soundness: The consequence of using a context-free language for T intro-
Search WWH ::
Custom Search