# Presentation: 507879

## Disciplined Software Engineering Lecture #12

**Software Engineering Institute**
**Carnegie Mellon University**
**Pittsburgh, PA 15213**
**Sponsored by the U.S. Department of Defense**

## Design Verification 

**Design verification is covered in 2 lectures.  This lecture addresses**
**the reasons for design verification**
**state machine correctness**
**execution tables**
**proof by induction**
**The next lecture covers**
**trace tables**
**mathematical program verification**
**program proofs**

## Need for Design Verification - 1

**As you work to improve your personal software process, you will likely find it hard to significantly reduce the numbers of design defects you make. **
**By using checklists and taking increased care, you can improve the yield of your code reviews.  **
**To improve the yield of design reviews, you need to use disciplined verification methods.**

## Slide 4

## Slide 5

## Need for Design Verification - 2

**An orderly approach to design verification is essential because**
**many common design defects are caused by overlooked conditions**
**what seem like unlikely situations become more likely with high-powered computing systems**
**conditions that were not possible with an initial program version may be induced by later modifications**

## Need for Design Verification - 3

**By following a structured design verification procedure, you are more likely to**
**see overlooked conditions**
**identify rarely exposed risks**
**recognize possible future exposures**
**By recording data on your design reviews, you can simplify later design inspections.**

## Using Design Verification - 1

**Design verification methods should be used **
**during design **
**during design reviews**
**during design inspections**
**Your design verification methods should focus on the defect types that have caused you the most trouble in test.**

## Using Design Verification- 2

**The topics covered in this and the next lecture were selected because they address the design defect categories that caused me the most trouble**
**state machine structures**
**loop constructs**
**I would use additional verification methods for the following defect types if they were available**
**pointers**
**interfaces**

## Design Verification Topics

**The design verification topics covered in this and the next lecture are**
**verifying state machine correctness**
**execution tables**
**proof by induction**
**trace tables**
**mathematical program verification**

## State Machine Correctness

**Any program that changes the state of the computing system is a state machine.**
**A program is a state machine if it can behave differently with identical inputs.  **
**Seemingly simple state machines can have sophisticated behavior.  It is thus important to verify them carefully.**

## State Machine Verification 

**The steps in state machine verification are to**
**check to ensure the state machine has no hidden traps or loops**
**check that the set of all states is complete and orthogonal**
**check that the set of all transitions from every state are complete and orthogonal**
**After verifying state machine correctness, ensure that the program performs the intended application functions.**

## Hidden Traps or Loops - 1

**To check for hidden traps and loops**
**construct the state template**
**construct a state machine diagram**
**determine if any exit states are unreachable from any other states**
**If any states cannot reach an exit state, this is not a proper state machine. **

## Hidden Traps or Loops - 2

**Example:  consider an object BSet as follows**
**2 states: EmptyState, MemberState**
**4 methods: Push, Pop, Add, Subtract**
**Push adds a member to BSet**
**Pop removes a member from BSet**
**Add adds a member to BSet if it does not already contain an identical member**
**Subtract removes a member from BSet if it contains an identical member**

## Hidden Traps or Loops - 3

**The state template for BSet would be as follows:**

**EmptyState**

**MemberState**

**EmptyState**

**MemberState**

**EmptyState**

**MemberState**

**n = 0**

**n >= 1**

**Pop or Subtract **

**Push or Add**

**Pop(n=1) or Subtract(n=1)(D in BSet)**

**Add or Push or Pop(n>1) or**
**Subtract(D not in BSet) or**
**Subtract(n>1)**

## Hidden Traps and Loops - 4 

**EmptyState**
**n = 0**

**MemberState**
**n > 0**

**Pop(n=1) or**
**Subtract(n=1)(D in BSet)**

**Pop or Subtract**

**Push or Add**

**Add or Push or Pop(n>1) or**
**Subtract(D not in BSet) or**
**Subtract(n>1)**

## Hidden Traps or Loops - 5

**It is thus clear that this state machine has no hidden traps or loops.**

## All Possible States - 1

**A common problem is to overlook some state machine state.**
**Examples are initial states, empty states, error states, and so forth.**
**Examine all possible conditions of the state parameters to ensure they are either included or truly impossible.**

## All Possible States - 2

**Checking the BSet example:**
**EmptyState has n = 0**
**MemberState has n > 0**
**since n cannot be < 0, this covers all cases**
**To ensure that none of the n > 0 states should be distinct, check to see if any of them exhibit different behavior from the others.**
**A check of the state template or state diagram shows that all n>0 states behave identically.  Added states are thus unnecessary.**

## State Orthogonality 

**For the states to be orthogonal, the state machine must not be able to be in 2 states at once.**
**In the example state machine, either **
**n = 0 or n > 0.  **
**The states are orthogonal because the machine must be in either the EmptyState  (n = 0) or the MemberState (n > 0); it cannot be in both at once.  **

## State Transitions - 1 

**In a proper state machine, the state transitions must all be complete and orthogonal.**
**For this to be true**
**every state must have a defined next state for every possible input**
**every state must have a unique next state for every possible input**

## State Transitions - 2 

**First, check EmptyState in the BSet example for completeness:**
**the conditions are Push, Pop, Add, and Subtract**
**states are defined for each condition, so the EmptyState transitions are  complete.**
**The following table shows they are complete:**

**Push**

**Pop**

**Add**

**Subtract**

**MemberState**

**EmptyState**

**MemberState**

**EmptyState**

## State Transitions - 3 

**Next, check EmptyState transitions for orthogonality.**
**The transition conditions to EmptyState are Pop and Subtract.**
**The transition conditions to MemberState are Push and Add. **
**Since these next state transition conditions do not overlap, the transition conditions are orthogonal.  **

## State Transitions - 4 

**For MemberState completeness, the possible cases are**

**Since these are all the possible cases, the **
**MemberState transitions are complete.**

## State Transitions - 5 

**For MemberState orthogonality, there must be no overlap between the transitions.**
**the transitions from MemberState to EmptyState occur when: Pop(n=1) or Subtract(n=1) and (D in BSet)**
**the transitions from MemberState to MemberState occur when: Add + Push + Pop(n>1) + Subtract(D not in BSet) + Subtract(n>1)**
**As is clear from the previous chart, these two cases have no condition in common and are thus orthogonal. **

## Class Exercise - 1

**The SignOn object is to have the following methods**
**Open - initiates a sign-on procedure**
**LogOn - requests a name**
**if the name is correct, PassWord requests the password**
**if the PassWord is correct, SignOn terminates with the value true**
**if there is any error, the program starts again at LogOn**
**for any two errors, SignOn terminates with the value false**

## Class Exercise - 2

**Construct the SignOn state template and state diagram.**
**Check for hidden traps and loops.**
**Check the states for completeness and   orthogonality.**
**Check the transitions for completeness and  orthogonality.**

## Class Exercise - State Diagram

**Class Exercise - State Diagram**

**StandBy**

**Error**

**Trial**

**Open**

**LogOn(No)**
**(false)**

**LogOn(No)**

**LogOn(Yes)**

**PassWord(Yes)**
**(true)**

**PassWord(No)**

**LogOn(Yes)**

**PassWord(Yes) (true)**
**PassWord(No) (false)**

**Start**

**NameOk**

## Exercise - State Template

**StandBy**

**Start**

**Open**

**Start**

**n = 0**

**n = 1**

**NameOk**

**Error**

**LogOn(Yes)**

**LogOn(No)**

**NameOk**

**n = 2**

**Error**

**PassWord(No)**

**StandBy (true)**

**Password(Yes)**

**Error**

**n = 3**

**Trial**

**LogOn(Yes)**

**StandBy (false)**

**LogOn(No)**

**Trial**

**n = 4**

**StandBy (true)**

**PassWord(Yes)**

**StandBy(false)**

**PassWord(No)**

## Execution Tables - 1

**An execution table is an orderly way to trace program execution.**
**it is a manual check of the program flow**
**it starts with initial conditions**
**a set of variable values is selected**
**each execution step is examined**
**every change in variable values is entered**
**program behavior is checked against the specification**

## Execution Tables - 2

**The advantages of execution tables are**
**they are simple **
**they give reliable proofs**
**The disadvantages of execution tables are**
**they only check one case at a time**
**they are time consuming**
**they are subject to human error**

## Execution Table Procedure

**To use an execution table**
**identify the key program variables and enter them at the top of the trace table**
**enter the principal program steps **
**determine and enter the initial conditions **
**trace the variable values through each program step**
**for repeating loops, add additional execution table steps for each additional loop cycle**
**for long loops, group intermediate steps if their results are obvious**

## Execution Table Example - 1

**Cycle 1**

**ClearSpaces(var Input: string; State: int)**

**#**

**1**

**2**

**3**

**4**

**5**

**6**

**7**

**Instructions**

**Condition**

**Input**

**Length**

**State**

**Length = length(Input)**

**‘ ****AB  ‘**

**5**

**0**

**if Length > 0**

**true**

**repeat(until State=3 or Length=0)**

**if Input[Length-1] = ‘ ‘**

**true**

**Length = Length - 1**

**if State < 2 State=State+1**

**4**

**true**

**1**

**else State = 3**

**until State=3 or Length=0**

**false**

## Execution Table Example - 2

**3 cycles are required before the until condition is satisfied.**
**Just as with a test case, the execution table will only prove the case for this specific variable combination.**
**Carefully check the initial conditions to ensure they are set by the program. **
**Double check the execution table for errors and omissions.**

## Proof by Induction

**This method applies to Boolean functions with integer parameters.**
**It states**
**if f(n) is true for n = k**
**and if **
**when n = z where z > k**
**and f(z) is true**
**you can show that f(z+1) is true**
**then f(n) is true for all values of n larger than k **

## Proof by Induction Example

**Example:**
**   ****for i=1 to Limit**
**       ****do xyz**
**   **
**If **
**you can show that this is true for Limit = 1 and**
**it is true for some arbitrary larger value z and**
**you can then show it would be true for z+1**
**then it is true for all positive values of Limit**

## A Proof by Induction Technique

**If **
**you have a design element using variable x**
**you verify that it works for x = k**
**Next**
**assume it works for some larger value x = z**
**try to find a value of z where program behavior would be improper at z + 1**
**If you cannot, the proof is completed.**

## Factorial Example - 1

**Prove that the following program produces N!**
**Factorial(N)**
**   ****F = 1**
**   ****for i = 1 to N**
**      ****F = F*i**
**   ****return = F**

## Factorial Example - 2

**Pick k = 1 and show that when N=1, F = N! **
**since 1 factorial is 1, this is correct**
**Next, assume that when N = z, F = z!**
**Finally, find any value of z where**
**      ****F(z) = z! and F(z+1) <> (z+1)!**
**Such cases would only occur when**
**the computing number system was exceeded**
**computing capacity was exceeded**

## Assignment #12

**Read Chapter 12 in the text.**
**Continue developing program 10A.**
**If you have time, start working on the Final Report, R5.  The specifications for  R5 can be found in Appendix D.**

## The Messages to Remember from Lecture 12 

**1.  Your design review yield will significantly **
**     ****improve if you use disciplined design **
**     ****review methods.**
**2.  The time spent verifying designs will be **
**     ****more than repaid by the testing time saved.**
**3.  Practice verification techniques and select**
**     ****the most effective for finding the defects **
**     ****you most commonly find in testing.**