New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here


by: Paxton Okuneva


Paxton Okuneva
GPA 3.57


Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Class Notes
25 ?




Popular in Course

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.




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


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


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'

Why people love StudySoup

Jim McGreen Ohio University

"Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

Kyle Maynard Purdue

"When you're taking detailed notes and trying to help everyone else out in the class, it really helps you learn and understand the I made $280 on my first study guide!"

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."


"Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.