Correctness Analysis: Inspection, Validation, Verification

This Chapter investigates three fundamental methods for computational analysis at different levels of abstraction of a hierarchical process development: mathematical VERIFICATION (by proofs of behavioural properties), experimental system VALIDATION (by test suites) and professional model INSPECTION (checking basic concepts against requirements). Stepwise refinements lead the development chain from abstractions to code.