tailieunhanh - Lecture Software testing and analysis - Chapter 2: A framework for testing and analysis

This chapter describes the nature of those trade-offs and some of their consequences, and thereby a conceptual framework for understanding and better integrating material from later chapters on individual techniques. | A Framework for Testing and Analysis c 2007 Mauro Pezze Michal Young Ch 2 slide 1 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 Pezze Michal Young Ch 2 slide 3 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 Pezze Michal Young Ch 2 slide 2 Validation and Verification Verification Includes testing inspections static analysis Actual Requirements Validation Includes usability testing user feedback c 2007 Mauro Pezze Michal Young Ch 2 slide 4 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. c 2007 Mauro Pezze Michal Young Ch 2 slide 5 ever You can t always get what you want Correctness properties are undecidable the halting problem can be embedded in almost every property of interest c 2007 Mauro Pezze Michal Young Ch 2 slide 7 Validation and Verification Activities Getting what you need . optimistic inaccuracy we may accept some programs that do not possess the property . 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 Ch 2 slide 8 Example of simplified property Unmatched Semaphore Operations original problem simplified property if . lock S . if . unlock S Static