Model Checking Approach:
• Specify program model and exhaustively evaluate that model against a speci?cation
–Check that properties hold
• The system will always shutdown when the pressure exceeds 100psi
–Produce counter examples when properties do not hold