楍档-FiniteStateVerification.pptVIP

(c) Mauro Pezzè Michal Young 2003 Finite State Verification 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 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 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 near-interactive analysis tools Analysis of models Applications for Finite State Verification Concurrent (multi-threaded, distributed, ...) Difficult to test thoroughly (apparent non-determinism based on scheduler); sensitive to differences between development environment and field environment First and most well-developed application of FSV Data models Difficult to identify “corner cases” and interactions among constraints, or to thoroughly test them Security Some threats depend on unusual (and untested) use Defining the global s