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
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
|
1
00:00:00,320 --> 00:00:01,630
Now that we got out of the way this
2
00:00:01,630 --> 00:00:04,460
initial set of basic definitions. Let's go back to our
3
00:00:04,460 --> 00:00:08,770
main concept, which is software verification. We said that software
4
00:00:08,770 --> 00:00:11,730
is buggy, and because software is buggy, we need to
5
00:00:11,730 --> 00:00:14,690
verify the software as much as we can. But how
6
00:00:14,690 --> 00:00:17,960
can we verify software? There are several ways to verify
7
00:00:17,960 --> 00:00:21,150
a software system. Among those, we will discuss four mainstream
8
00:00:21,150 --> 00:00:25,410
approaches. The first one is testing, also called dynamic verification.
9
00:00:25,410 --> 00:00:29,400
The second approach is static verification. The third approach is
10
00:00:29,400 --> 00:00:33,000
inspections. And finally, we're going to consider a fourth approach which is
11
00:00:33,000 --> 00:00:36,090
formal proofs of correctness. So what I'm going to do
12
00:00:36,090 --> 00:00:39,570
next, I'm going to first provide an overview of these approaches and
13
00:00:39,570 --> 00:00:41,930
then discuss some of them in more depth and please
14
00:00:41,930 --> 00:00:44,430
note that although we will discuss all four approaches we will
15
00:00:44,430 --> 00:00:47,350
spend most of our time on software testing. As software
16
00:00:47,350 --> 00:00:50,850
testing is the most popular and most used approach in industry.
17
00:00:50,850 --> 00:00:53,050
So let's start with our overview and in particular
18
00:00:53,050 --> 00:00:58,050
with testing. Testing a software system means exercising the system
19
00:00:58,050 --> 00:01:01,680
to try to make it fail. More precisely, let's consider
20
00:01:01,680 --> 00:01:04,440
a program. Its input domain, which is the set of
21
00:01:04,440 --> 00:01:06,990
all the possible inputs for the program and, its output
22
00:01:06,990 --> 00:01:09,470
domain, which is a set of all the possible corresponding
23
00:01:09,470 --> 00:01:13,010
outputs. Given this context, we can define what a test
24
00:01:13,010 --> 00:01:16,360
case is. A test case is a pair that consists
25
00:01:16,360 --> 00:01:19,090
of a, an input from the input domain D,
26
00:01:19,090 --> 00:01:22,620
and then, expected output O from the output domain.
27
00:01:22,620 --> 00:01:25,950
And O is the element in the output domain
28
00:01:25,950 --> 00:01:29,670
that a correct software would produce when ran against I.
29
00:01:29,670 --> 00:01:32,170
We can also define the concept of test suite,
30
00:01:32,170 --> 00:01:34,840
which is a set of test cases, and we're going to
31
00:01:34,840 --> 00:01:37,730
use these two concepts of test case and test
32
00:01:37,730 --> 00:01:41,400
suite quite a bit in the rest of the lessons.
33
00:01:41,400 --> 00:01:44,980
Subject verification, tries to identify specific classes of problems
34
00:01:44,980 --> 00:01:47,620
in the program. Such as null pointer dereferences. And
35
00:01:47,620 --> 00:01:49,750
unlike testing, what it does is that it does
36
00:01:49,750 --> 00:01:53,610
not just consider individual inputs, it instead considers all
37
00:01:53,610 --> 00:01:56,594
possible inputs for the program. So it consider in
38
00:01:56,594 --> 00:01:59,366
a sense all possible executions of the program and
39
00:01:59,366 --> 00:02:02,402
all possible behaviors of the program, that's why we
40
00:02:02,402 --> 00:02:06,560
save the verification unlike testing it's complete. The 3rd technique
41
00:02:06,560 --> 00:02:08,755
we are going to consider is inspections,
42
00:02:08,755 --> 00:02:12,804
and inspections are also called reviews or walkthroughs.
43
00:02:12,804 --> 00:02:15,010
And unlike the previous techniques, inspections are a
44
00:02:15,010 --> 00:02:18,660
human intensive activity, more precisely, they are a
45
00:02:18,660 --> 00:02:22,520
manual and group activity in which several
46
00:02:22,520 --> 00:02:25,700
people from the organization that developed the software,
47
00:02:25,700 --> 00:02:29,190
look at the code or other artifacts developed
48
00:02:29,190 --> 00:02:31,888
during the software production and try to identify
49
00:02:31,888 --> 00:02:35,950
defects in these artifacts. And interestingly inspections
50
00:02:35,950 --> 00:02:37,580
have been shown to be quite effective in
51
00:02:37,580 --> 00:02:39,820
practice and that's the reason why they're used
52
00:02:39,820 --> 00:02:42,550
quite widely in the industry. Finally, the last
53
00:02:42,550 --> 00:02:45,100
technique I want to mention is Formal
54
00:02:45,100 --> 00:02:49,650
Proof (of correctness). Given a software specification, and
55
00:02:49,650 --> 00:02:53,370
actually a formal specification, so a document that
56
00:02:53,370 --> 00:02:57,410
formally defines and specifies the behavior, the expected
57
00:02:57,410 --> 00:03:00,320
behavior of the program. A form of proof of
58
00:03:00,320 --> 00:03:05,400
correctness proves that the program being verified, actually implements
59
00:03:05,400 --> 00:03:07,922
the program specification and it does that through a
60
00:03:07,922 --> 00:03:12,880
sophisticated mathematical analysis of the specifications and of the code.
|
