Testing, Simulation, and Formal Methods

Testing, simulation, and formal methods are three common techniques in verification. However, distinguishment between them is not very clear to many people working in other CS disciplines. I found two examples in Wang Farn's slides very helpful in explaining their differences──the three techniques are visualized by three correspondent approaches to answer the following two questions.

Q: Do the 3 angles in every triangle sum to 180 ?

Testing (check all triangles you see)

• Expensive 
• Low coverage
• Late in development cycles

Simulation (check all triangles you draw)

• Economic 
• Low coverage
• Don't know what you haven't seen

Formal Verification (prove it)

• Expensive
• 100% coverage
• Proofs may be automatically verified

Q: What is the robustness of a new design of call?

• Testing (let real cars hit a real wall)
• Simulation (let virtual cars hit a virtual wall)
• Formal Verification (verify the car models)

Wang Yin also wrote a blog article trying to explain the difference between testing and static analysis (one of the popular formal methods) in plain words.