-
Notifications
You must be signed in to change notification settings - Fork 0
/
tutorial.html
165 lines (120 loc) · 8.85 KB
/
tutorial.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
<!DOCTYPE html>
<html lang="en-us">
<head>
<meta charset="UTF-8">
<title></title>
<meta name="description" content=""/>
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="theme-color" content="#157878">
<link href='https://fonts.googleapis.com/css?family=Open+Sans:400,700' rel='stylesheet' type='text/css'>
<link rel="stylesheet" href="/temporalTest/assets/css/style.css?v=e6385aa5d099879fe352412a0d0eca6a66f2d907">
</head>
<body>
<section class="page-header">
</section>
<section class="main-content">
<h1 id="tutorials">Tutorials</h1>
<p><font size="4">We provide two tutorials for RGSE. We first apply RGSE to analyze a <b>motivation</b> program with respect to the <font color="#0000FF">reader
</font> property, i.e., the <b>InputStreamReader</b> cannot read while closed.
Then, we present the analysis of program <b>Rohino-a</b> with respect to
the <font color="#0000FF">Enumeration</font> property, i.e., invoking hasMoreElements before nextElement.</font></p>
<p><font size="4">It is worth noting that we introduce how to make a variable symbolic
detailedly in the <a href="https://jrgse.github.io/API.html">API documentation.</a></font></p>
<hr />
<h2 id="a-motivation-example"><strong>A Motivation Example</strong></h2>
<p><font size="4">The motivation example is shown below. We make the three integer variables <b>m</b>, <b>n</b>, and <b>tag</b> symbolic, and initialize them to 1, 1, and 5, respectively.
Obviously, when <b>tag</b> equals 0 and <b>n</b> is positive, a violation of the <font color="#0000FF">reader</font> property exists, i.e.,
the <b>InputStreamReader</b> object <b>w</b> reads while it has been closed.</font></p>
<p><img src="https://raw.githubusercontent.com/srv4j/images/master/moti.jpg" alt="program" /></p>
<hr />
<h2 id="1-analysis-driver"><strong>(1). Analysis Driver</strong></h2>
<p><font size="4">The driver gives the entry point of the analysis, and contains two main modules:
<b>property specification</b> and <b>running configuration</b>.<font size="4"></p>
<p><font size="4">The whole analysis driver for the motivation example can be downloaded from
<a href="https://github.com/jrgse/demo/blob/master/TestMotiExamplewithSlicing.java">this link</a>.<font size="4"></p>
<ul>
<li><code class="highlighter-rouge"><font size="4" color="green"><b>Property Specification</b></font></code>:</li>
</ul>
<p><font size="4">We specify the property to be checked as a finite state machine (FSM),
where <b>I</b>, <b>R</b>, and <b>C</b> represent the <b>init</b>,
<b>read</b>, and <b>close</b> event of the <font color="#0000FF">
reader</font> property. The property events can be recognized with the help of Java monitors, i.e.,
comparing the invoked method's name and class type with the property description.
<b>createState</b> and <b>new FSATransition</b> are used to create FSA states and transitions, and details can
be found in <a href="API.html">API Documentation</a>. <b>Global.shortestPathLength.put(int, int)</b> is used to record the distance from
a state to the accepted state, where the first parameter is the state identifier and the second parameter is the distance.
<font size="4"></p>
<p><img src="https://raw.githubusercontent.com/srv4j/images/master/FSA_moti.jpg" alt="fsm_spec" />
<img src="https://raw.githubusercontent.com/srv4j/images/master/FSM.jpg" alt="fsm" /></p>
<hr />
<ul>
<li><code class="highlighter-rouge"><font size="4" color="green"><b>Running Configuration</b></font></code>:</li>
</ul>
<p><font size="4">After writing the property specification, we set the running configuration of <b>RGSE</b>.
Specifically, the five parameters in args represent <b>call string bound</b>,
<b>property guided</b>, <b>refinement flag</b>, <b>iteration threshold</b>, <b>time threshold</b>, <b>result file name</b>,
and <b>slicing flag</b>, respectively. As is shown below, args <i>(“1”, “1”
“0”, “-1”, “0,0,10,0”, “”, “0”)</i> sets the <b>call string bound</b> to be 1,
enables <b>property guiding</b>, and sets the <b>time threshold</b> to be 10 seconds.</font></p>
<p><img src="https://raw.githubusercontent.com/srv4j/images/master/args_moti.jpg" alt="args_rgse" /></p>
<hr />
<h2 id="2-running-rgse"><strong>(2). Running RGSE</strong></h2>
<p><font size="4">We can run <b>RGSE</b> in two ways, i.e., running the analysis driver as a Java application
in Eclipse or running the docker script in command line. The general command
for running the script is <b>“./docker_script arg1 arg2”</b>. The two paremeters are used to specify the running mode.
Specifically, <b>“0 0”</b> is for <b>DFS</b> mode, <b>“0 1”</b> is for <b>path slicing</b> mode, and <b>“1 0”</b> is for our <b>guiding</b> mode.<font size="4"></p>
<hr />
<h2 id="3-analysis-result"><strong>(3). Analysis Result</strong></h2>
<p><font size="4">The results include the time consumption, explored paths, iteration and time for finding the first accepted path
, and so on. For the <b>motivation</b> example and the <font color="#0000FF">reader</font> property, the results below show
that <b>RGSE</b> can find the program path satisfying the FSM in the <b>2nd</b> iteration.
On the other hand, neither <b>DFS</b> nor <b>slicing</b> can find the property violation
within the time threshold.</font></p>
<p><img src="https://raw.githubusercontent.com/srv4j/images/master/moti_result.jpg" alt="results" /></p>
<hr />
<h2 id="program-rohino-a"><strong>Program Rohino-a</strong></h2>
<p><font size="4">The Javascript interpreter program <b>Rohino-a</b> is from the <b>Ashes suite</b> benchmark. The program can be downloaded
from <a href="https://github.com/jrgse/demo/tree/master/example-rhino">this link</a>.</font></p>
<hr />
<h2 id="1-analysis-driver-1"><strong>(1). Analysis Driver</strong></h2>
<p><font size="4">The driver gives the entry point of the analysis, and contains two main modules:
<b>property specification</b> and <b>running configuration</b>.</font></p>
<ul>
<li><code class="highlighter-rouge"><font size="4" color="green"><b>Property Specification</b></font></code>:</li>
</ul>
<p><font size="4">We specify the property to be checked as a finite state automaton (FSA),
where <b>H</b> and <b>N</b> represent the
<b>hasMoreElements</b> and <b>nextElement</b>
event of the <font color="#0000FF">Enumeration</font> property.
<b>createState</b> and <b>new FSATransition</b> are used to create FSA states and transitions, and details can
be found in <a href="API.html">API Documentation</a>. <b>Global.shortestPathLength.put(int, int)</b> is used to record the distance from
a state to the accepted state, where the first parameter is the state identifier and the second parameter is the distance.
<font size="4"></p>
<p><img src="https://raw.githubusercontent.com/srv4j/images/master/FSM_specRohino.jpg" alt="fsm_spec" />
<img src="https://raw.githubusercontent.com/srv4j/images/master/FSM_bloat.jpg" alt="fsm" /></p>
<hr />
<ul>
<li><code class="highlighter-rouge"><font size="4" color="green"><b>Running Configuration</b></font></code>:</li>
</ul>
<p><font size="4">After writing the property specification, we set the running configuration of <b>RGSE</b>. Specifically,
the five parameters in args represent <b>call string bound</b>,
<b>property guided</b>, <b>refinement flag</b>, <b>iteration threshold</b>, <b>time threshold</b>, <b>result file name</b>,
and <b>slicing flag</b>, respectively. As is shown below, args <i>(“1”, “1”
“0”, “-1”, “0,0,1800,0”, “”, “0”)</i> sets the <b>call string bound</b> to be 1, enables <b>property guiding</b>,
and sets the <b>time threshold</b> to be 30 minutes.</font></p>
<p><img src="https://raw.githubusercontent.com/srv4j/images/master/args_rohino.jpg" alt="args" /></p>
<hr />
<h2 id="2-running-rgse-1"><strong>(2). Running RGSE</strong></h2>
<p><font size="4">We can run <b>RGSE</b> in two ways, i.e., running the analysis driver as a Java application in Eclipse or
running the docker script in command line. The general command
for running the script is <b>“./docker_script arg1 arg2”</b>. The two paremeters are used to specify the running mode.
Specifically, <b>“0 0”</b> is for <b>DFS</b> mode, <b>“0 1”</b> is for <b>path slicing</b> mode, and <b>“1 0”</b> is for the <b>guiding</b> mode.</font></p>
<hr />
<h2 id="3-analysis-result-1"><strong>(3). Analysis Result</strong></h2>
<p><font size="4">The results include the time consumption, explored paths, the iteration and time for finding the first accepted path,
and so on. The results below show that <b>RGSE</b> can find the program path satisfying the FSM in <b>1707X</b>
seconds (about <b>28 minutes</b>). On the other hand, neither <b>DFS</b>
nor <b>slicing</b> can find the property violation even within <b>1 hour</b>.</font></p>
<p><img src="https://raw.githubusercontent.com/srv4j/images/master/rohino_result.jpg" alt="results" /></p>
</body>
</html>