Safety Properties: This property asserts that nothing bad will happen during the execution of the program (e.g., no deadlocks, or no attempts to take an item from an empty buffer).
Safety properties are used mainly to ensure consistency of the program state, for example by making sure that:
- Shared resources are updated atomically (mutual exclusion), or
- The state of shared resources is kept consistent by delaying certain operations (condition synchronization.