SOFTWARE TESTVERIFI CEN 6070
Popular in Course
CHEM - 10030 - 002
verified elite notetaker
Popular in Computer Engineering
This 6 page Class Notes was uploaded by Paxton Okuneva on Saturday September 19, 2015. The Class Notes belongs to CEN 6070 at University of Florida taught by Staff in Fall. Since its upload, it has received 7 views. For similar materials see /class/207043/cen-6070-university-of-florida in Computer Engineering at University of Florida.
Reviews for SOFTWARE TESTVERIFI
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/19/15
Lectures 24 and 25 More Functional Verification Magic and an Overview of Cleanroom Software Engineering We conclude our study of functional verification this week by briefly considering a remarkable connection between the functions computed by programs with while loops and the loop invariants studied in Lecture 18 Functional Verification IV Revisiting Loop Invariants In particular we will see how the Invariant Status Theorem provides a way to systematically derive loop invariants when the function computed by the loop is known Finally we consider a paper written by Harlan Mills associate Rick Linger about a ve interesting SE development method that utilizes function theoretic verification Cleanroom Software Engineering Week 13 Functional Verification IV Context In Week 10 we learned that synthesizing a loop invariant is a trial and error process We now consider a way to systematically derive loop invariants when the function computed by the loop is known Purpose To introduce and illustrate the application of the Invariant Status Theorem in deriving loop invariants These invariants may be used with the while loop ROI to prove the correctness of whiedo statements Since in many situations a loop invariant may hold by virtue of its initialization we also consider a limited invariant of an initialized while loop h while p do 9 Competency Objectives At the end of this lesson you will be able to 1 State and apply the Invariant Status Theorem to derive an invariant qX for a simple while loop with a known function 2 Derive a limited invariant for an initialized while loop with a known function Key Points 1 Invariant Status Theorem Let f while p do 9 If XOEDf XEDf and qX fXfXo then q is an invariant of while p do 9 and has the following properties a qXo is true and b qXpX 2 qogX and 6 qXpX 2 XfX0 2 While Loop Initialization Given f while p do 9 X0 E Df a limited invariant of the initialized while loop h while p do 9 is 100 fXf0hXo Such an invariant has the following properties a qohXo is true and b qXpX 2 qogX and C 100 pX 2 X f0hXo Cleanroom Software Engineering Context Cleanroom Software Engineering is a software development philosophy first introduced in the 19805 within IBM by Harlan Mills It is based on the notion that defects in software should be avoided rather than detected and repaired Development teams employ function theoretic correctness verification techniques Purpose To briefly describe a successful use of formal verification techniques in a practical scalable software development method Competency Objectives At the end of this lesson you will be able to 1 State the underlying philosophy of Cleanroom Software Engineering 2 Describe important characteristics of Cleanroom including quotbox structurequot specification and design incremental development and statistical usage testing Key Points Cleanroom Software Engineering is based on the notion that defects in software should be avoided rather than detected and repaired Software development should not be viewed as a trial and error undertaking H 2 Cleanroom makes use of function theoretic correctness verification components are not executed or developer tested 3 Every correctness condition of every control structure is veri ed every team member must agree that each condition is correct 4 Statistical usage testing utilizes a sample population of user executions based on expected frequency Quality is measured by determining if executions are correct 5 Box structure specification and design incorporates black box external behavior state box retained data and clear box processing forms SelfCheck Quiz Questions 1 6 pts For program P below use the Invariant Status Theorem to synthesize a limited invariant that COULD be used to prove that the program is weakly correct with respect to pre condition true and post condition yx k using the while loop rule of inference y 0 t X while tltgtk do t t 1 y y1 endwhile 24 pts In quotCleanroom Software Engineering for Zero Defect Softwarequot Linger claims that statistical usage testing is quotmore that 20 times more effectivequot than coverage testing at doing something What is it more effective at doing and why is this so Lectures 5 and 6 More BlackBox Test Case Design Strategies Our focus on black box testing strategies continues this week with the consideration of a combinatorial approach known as Cause Effect Analysis Black Box Testing Techniques 11 Following this we consider two additional strategies boundary value analysis and intuition and experience Black Box Testing Techniques III BlackBox Testing II and III Context We continue our exploration of black box test case design strategies this week focusing especially on a combinatorial approach that can be viewed as a logical extension of partition testing Purpose The lectures highlight the rationale and process of Cause Effect Analysis Two examples are used to illustrate its application and the various ways it can be employed to meet a variety of coverage requirementscost constraints We also consider two additional black box strategies known to be effective in revealing some very common types of errors boundary value analysis and test case design based on intuition and experience Com pete ncy O bjectives At the end of this lesson you will be able to H N E 5 9quot Key Points Explain the rationale of combinatorial approaches such as Cause Effect Analysis Apply the Cause Effect Analysis process steps to develop a formal model reflecting the logical relationships and constraints among input quotCausesquot and output quotEffectsquot Choose from among a variety of test case selection strategies according to the number and nature of Cause combinations being considered Describe guidelines for identifying boundary values to be explored during testing Utilize intuition and experience to identify potential errors and design test cases to reveal them H Cause Effect Analysis is a combinatorial approach that provides a systematic means for generating test cases to cover different combinations of input Causes resulting in output Effects 2 A CAUSE may be thought of as a distinct input condition or an equivalence class of input conditions an EFFECT may be thought of as a distinct output condition or change in program state 5 Causes and Effects are represented as Boolean variables the logical relationships among them CAN but need not be represented as one or more Boolean graphs 5 Several test case selection strategies may be employed to identify combinations of Causes to be tested these range from the very conservative to the very risky U39l A quotmiddle of the roadquot strategy that may be appropriate in many situations involves identifying feasible combinations of connected Cause values associated with each Effect possibly subject to culling rules that eliminate combinations of lesser interest 9 Boundary Value Analysis involves generating test cases to explore boundary conditions an extremely rich source of errors N Test Case Design Based on Intuition and Experience involves utilizing intuition and experience to identify potential errors and design test cases to reveal them Examples include plausible but incorrect assumptions made by developers and errors associated with unusual usage or environmental scenarios SelfCheck Quiz Questions 1 Consider the following Cause Effect model a How many test cases would be required to achieve AFCCV All Feasible Combinations of Cause Values coverage b How many test cases would be required to achieve AEMC All Effects covered with the Minimum number of test Cases coverage c How many test cases would be required to cover every feasible combination of connected Cause values associated with both Effects Briefly describe the quotRangequot guideline as in quotinput X will range in value fromtoquot for identifying boundary values Briefly describe two of the three guidelines for designing tests based on intuition and experience described in class
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'