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
|
1
00:00:00,280 --> 00:00:02,750
So let me start with some examples that motivate the
2
00:00:02,750 --> 00:00:06,330
need for very fine software. The first example I want to
3
00:00:06,330 --> 00:00:09,580
use is the famous Arian five. And if you remember
4
00:00:09,580 --> 00:00:13,060
that's a rocket that exploded not too long after departure.
5
00:00:13,060 --> 00:00:15,800
Because of a software error. And even without going to
6
00:00:15,800 --> 00:00:19,400
such dramatic examples. I'm sure you're all familiar with this
7
00:00:19,400 --> 00:00:22,470
kind of situation. Or this one, or again in this
8
00:00:22,470 --> 00:00:26,070
one. And here I'm not really picking on any specific organization,
9
00:00:26,070 --> 00:00:32,280
operating system or software. The point I want to make is that software is
10
00:00:32,280 --> 00:00:34,730
buggy. In fact, a federal report from
11
00:00:34,730 --> 00:00:37,810
a few years ago assessed that software bugs
12
00:00:37,810 --> 00:00:41,300
are costing the US economy, $60 billion
13
00:00:41,300 --> 00:00:44,120
every year. In addition, studies have shown that
14
00:00:44,120 --> 00:00:47,810
software contains on average one to five
15
00:00:47,810 --> 00:00:51,472
bugs every 1000 lines of code. Building 100%
16
00:00:51,472 --> 00:00:55,940
correct mass-market software is just impossible. And if
17
00:00:55,940 --> 00:00:58,270
this is the case, what can we do?
18
00:00:58,270 --> 00:01:03,520
What we need to do is to verify software as much as possible. In this part of
19
00:01:03,520 --> 00:01:05,750
the course, we will discuss how we can
20
00:01:05,750 --> 00:01:09,480
do this. We will discuss different alternative ways
21
00:01:09,480 --> 00:01:13,980
of very fine software systems. With particular attention
22
00:01:13,980 --> 00:01:16,570
to the most common type of verification. Which is
23
00:01:16,570 --> 00:01:19,470
software testing. Before doing that however, let
24
00:01:19,470 --> 00:01:21,090
me go over some basic terms that are
25
00:01:21,090 --> 00:01:23,190
commonly used. And I have to say,
26
00:01:23,190 --> 00:01:26,330
often misused in the context of software verification.
|
