tailieunhanh - Lecture Software testing and analysis - Chapter 8: Finite state verification

In this chapter you will learn: Understand the purpose and appropriate uses of finite-state verification (fsv), understand modeling for fsv as a balance between cost and precision, distinguish explicit state enumeration from analysis of implicit models. | Finite State Verification SOFTWARE TESTING ANOANALYSIS c 2007 Mauro Pezze Michal Young Ch 8 slide 1 Limits and trade-offs Most important properties of program execution are undecidable in general Finite state verification can automatically prove some significant properties of a finite model of the infinite execution space - balance trade-offs among generality of properties to be checked class of programs or models that can be checked computational effort in checking human effort in producing models and specifying properties SOFTWARE TESTING ANOANALYSIS c 2007 Mauro Pezze Michal Young Ch 8 slide 3 Learning objectives Understand the purpose and appropriate uses of finite-state verification fsv - Understand how fsv mitigates weaknesses of testing - Understand how testing complements fsv Understand modeling for fsv as a balance between cost and precision Distinguish explicit state enumeration from analysis of implicit models - And understand why implicit models are sometimes but not always more effective SOFTWARE TESTING AND ANALYSIS Resources and results Cost trade-offs Human effort and skill are required - to prepare a finite state model - to prepare a suitable specification for automated analysis Iterative process - prepare a model and specify properties - attempt verification - receive reports of impossible or unimportant faults - refine the specification or the model Automated step - computationally costly computational cost impacts the cost of preparing model and specification which must be tuned to make verification feasible - manually refining model and specification less expensive with MID-ANALYSIS near-interactive analysis tools IJesS c 2007 Mauro Pezze Michal Young Ch 8 slide 5 Applications for Finite state Verification Concurrent multi-threaded distributed . - Difficult to test thoroughly apparent nondeterminism based on scheduler sensitive to differences between development environment and field environment - First and most well-developed application of .