Static API Specification Mining: Exploiting Source Code Model Checking - Mining Software Specifications: Methodologies and Applications - page 129

5.2.3 Implementation
To generate static traces, we adapted a publicly available model checker
called MOPS [20]. To mine FCPOs, we adopted a FCPO miner called
FRECPO [47]. The FCPO miner employed in our framework does not handle
duplicate strings. We handled this implementation limitation by appropriately
modifying the scenario extraction algorithm. The process of generating error
traces from a nal conguration hq;!i (! is the stack content containing a list
of return addresses) of PDA P is called backtracking [18]. With the knowledge
of a user-specied set of APIs, A = fa 1 ;a 2 ;a 3 ;:::;a k g, our framework extracts
A(t) from any trace t produced by MOPS. The PDMC process produces a
graph in which certain paths map to violation paths in the program [18].
Multiple program paths (and hence graph paths) can violate a given property
specified by a FSM (such as the one shown in Figure 5.5), and many such
violations could be similar because they indicate the same programming bug.
So instead of reporting all program traces that violate a given property, the
MOPS model checker clusters similar traces and reports the shortest trace as
a candidate trace for each violation. This mechanism would save the user's
time considerably because the user need not review each trace manually.
However, for our purposes, given a Trigger, we need all the traces in the
program that contain the APIs specified in the Trigger. We modified the back-
tracking algorithm of MOPS, wherein, instead of clustering traces, we consider
all program paths that satisfy the Trigger, and produce a random number of
traces by random walking the graph generated by the PDMC process. In our
experiments, we specified a threshold (20 in our experiments) for the number
of traces to be generated from each program. MOPS assumes that a loop may

appres beforelight bitmap dpsexec xload xlogo

dpsinfo editres glxgears glxinfo xlsatoms xlsclients

iceauth ico listres luit xlsfonts xmag

makepsres oclock proxymngr rstart xman xmessage

setxkbmap showfont smproxy texteroids xmh xmodmap

twm viewres x11perf xauth xpr xrandr

xbiff xcalc xclipboard xclock xrdb xrefresh

xcmsdb xconsole xditview xdpyinfo xset xsetmode

xev xeyes xf86dga xfd xsetpointer xsetroot

xfindproxy xfontsel xfsinfo xfwp xstdcmap xterm

xgamma xgc xhost xinit xtrap xvidtune

xkbevd xkbvleds xkbutils xkill xvinfo xwud

FIGURE 5.9: X11 client programs used in our evaluation.