View article

The distinction of safety and liveness properties is often adopted in speci cation and design methods for distributed systems. We present a short survey on the\history" of these concepts and on papers that contributed to their general acceptance.

The notions of safety and liveness properties have been rst introduced by Lamport 14]. Informally, a safety property expresses that\something (bad) will not happen" during a system execution. A liveness property expresses that eventually\something (good) must happen" during an execution. The distinction of safety and liveness properties was motivated by the di erent techniques for proving those properties. For example, Owicki and Lamport 16] propose the technique of proof lattices for liveness properties. Later, Lamport makes his informal characterization of safety properties more precise 4]. An execution of a distributed system is formalized as an in nite sequence of states. Any set of such sequences is a property. A property is called a safety property (Section 2.2 in 4]), if and only if each execution violating the property has a nite pre x1 violating that property and, vice versa2, if a nite pre x of an execution violates the property then the execution itself violates the property. This corresponds to the intuition that the\bad thing"(ie violating the property) can be detected in a nite initial part of the execution and the occurrence of the\bad thing" in a pre x of an execution is irremediable. The notion of safety properties is also convincing because a safety property can be generated by a transition systems with nite internal nondeterminism 3]. This\property of safety properties" seems to be one of the main justi cations for …