Safety property


In distributed computing, safety properties informally require that "something bad will never happen" in a distributed system or distributed algorithm. In a database system, a promise to never return data with null fields is an example of a safety guarantee. Another example is that of deadlock freedom—it should never occur that all processes or a distributed system are unable to continue because they are waiting for action from another process.
Safety properties are types of linear time properties studied in the area of model checking, along with liveness properties. Unlike liveness properties, safety properties can be violated by a finite execution of a distributed system. All properties can be expressed as the intersection of safety and liveness properties.