-
Safety Properties
-
What a system must not do (bad things should never happen).
-
They don't require that the system ever actually do anything.
-
If a safety property is violated, it is violated at some particular point in the behavior.
-
These properties, which can be specifed with almost no temporal logic, are all that most engineers need to know about.
-
-
Liveness Properties
-
What a system should do (good things do happen eventually)
-
Fairness is enough for most specifications
-