Software Measurement and Testing
A Framework
for Testing and Analysis
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 1
Learning objectives
• Introduce dimensions and tradeoff between test and analysis activities
• Distinguish validation from verification activities
• Understand limitations and possibilities of test and analysis
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 2
Verification and validation
• Validation:
does the software system meets the user’s real needs?
are we building the right software?
• Verification:
does the software system meets the requirements specifications?
are we building the software right?
(c) 2007 Mauro Pezzè & Michal Young
Ch 2, slide 3
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 4
Validation and Verification
SW Specs
System
Actual Requirements
Validation
Includes usability testing, user feedback
usability
Verification
Includes testing, inspections, static analysis
dependability
(c) 2007 Mauro Pezzè & Michal Young
Ch 2, slide 5
Verification or validation depends on the specification
Example: elevator response
Unverifiable (but validatable) spec: … if a user presses a request button at floor i, an available elevator must arrive at floor i soon…
Verifiable spec: … if a user presses a request button at floor i, an available elevator must arrive at floor i within 30 seconds…
12 3 4 56 78
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 6
Validation and Verification Activities
Actual Needs and Constraints
System Specifications
User Acceptance (alpha, beta test )
System Test
Analysis / Review
Delivered Package
System Integration
Subsystem Design/Specs
Integration Test
Subsystem
Unit/ Component Specs
Analysis / Review
Module Test
Unit/ Components
validation
verification
User review of external behavior as it is determined or becomes visible
(c) 2007 Mauro Pezzè & Michal Young
Ch 2, slide 7
Review
The V-model
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 8
ever
You can’t always get what you want Property
Pass/Fail
Program
Correctness properties are undecidable
the halting problem can be embedded in almost every property of interest
Decision Procedure
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 9
A little reminder of undecidability
• A property is undecidable if it is impossible to build a Turing machine (and hence also a computer program) that will ACCEPT if an input satisfies the property and REJECT if an input falsifies the property
– most correctness properties are undecidable by a reduction from the halting problem
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 10
Theorem proving: Unbounded effort to verify general
properties.
Model checking: Decidable but possibly intractable checking of simple temporal properties.
Precise analysis of simple syntactic properties.
Simplified properties
Perfect verification of arbitrary properties by logical proof or exhaustive testing (Infinite effort)
• optimistic inaccuracy: we may accept some programs that do not possess the property (i.e., it may not detect all violations).
– testing
• pessimistic inaccuracy: it is not guaranteed to accept a program even if the program does possess the property being analyzed
– automated program analysis techniques
• simplified properties: reduce the degree of freedom for simplifying the property to check
Getting what you need …
Data flow analysis
Pessimistic inaccuracy
(c) 2007 Mauro Pezzè & Michal Young
Ch 2, slide 11
Typical testing techniques
Optimistic inaccuracy
Example of simplified property: Unmatched Semaphore Operations
if ( …. ) {
…
lock(S); }
…
if ( … ) {
…
unlock(S); }
Static checking for match is necessarily inaccurate …
…
original problem
simplified property
Java prescribes a more restrictive, but statically checkable construct.
synchronized(S) {
…
}
(c) 2007 Mauro Pezzè & Michal Young
Ch 2, slide 12
Another example of a simplified property: initialisation of variables
int I, sum; int first=1;
for (i=0; i<10; i++){
if (first){
sum=0; first =0;
} sum++;
is it safe?
yes – sum is initialised in the first iteration
static analysis checks
that variables are initialised in all paths
}
(c) 2007 Mauro Pezzè & Michal Young
Ch 2, slide 13
Some Terminology
• Safe: A safe analysis has no optimistic inaccuracy, i.e., it accepts only correct programs.
• Sound: An analysis of a program P with respect to a formula F is sound if the analysis returns true only when the program does satisfy the formula. (conservative)
• Complete: An analysis of a program P with respect to a formula F is complete if the analysis always returns true when the program actually does satisfy the formula. (optimistic)
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 14
Summary
• Most interesting properties are undecidable, thus in general we cannot count on tools that work without human intevention
• Assessing program qualities comprises two complementary sets of activities: validation (does the software do what it is supposed to do?) and verification (does the system behave as specified?)
• There is no single technique for all purposes: test designers need to select a suitable combination of techniques
(c) 2007 Mauro Pezzè & Michal Young Ch 2, slide 15
Home reading
• Chapter 2 of the book Software Testing and Analysis, by Mauro Pezze and Michal Young
– A Framework for Testing and Analysis
(c) 2007 Mauro Pezzè & Michal Young Ch 1, slide 16