From b2d80610db6beda38573890ed169815e495bc663 Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <mcsinyx@disroot.org>
Date: Sun, 24 May 2020 16:34:31 +0700
Subject: [usth/ICT2.7] Engineer software

---
 .../10 - Verification Approaches - lang_en_vs4.srt | 239 +++++++++++++++++++++
 1 file changed, 239 insertions(+)
 create mode 100644 usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt

(limited to 'usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt')

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
new file mode 100644
index 0000000..a671818
--- /dev/null
+++ b/usth/ICT2.7/P4L1 General Concepts Subtitles/10 - Verification Approaches - lang_en_vs4.srt	
@@ -0,0 +1,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.
-- 
cgit 1.4.1