1 files changed, 0 insertions, 239 deletions
diff --git a/usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt b/usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt
deleted file mode 100644
index a671818..0000000
--- a/usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt
+++ /dev/null
@@ -1,239 +0,0 @@
-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.