Jump to content

Safety property

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Monkbot (talk | contribs) at 03:05, 17 December 2020 (Task 18 (cosmetic): eval 4 templates: del empty params (4×);). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

In distributed computing, safety properties informally require that "something bad will never happen" in a distributed system or distributed algorithm.[1][2] In a database system, a promise to never return data with null fields is an example of a safety guarantee.[3] 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.[4]

Safety properties are types of linear time properties studied in the area of model checking, along with liveness properties.[4] 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.[3]

References

  1. ^ Rodrigues, Christian Cachin; Rachid Guerraoui; Luís (2010). Introduction to reliable and secure distributed programming (2. ed.). Berlin: Springer Berlin. pp. 22–24. ISBN 978-3-642-15259-7.{{cite book}}: CS1 maint: multiple names: authors list (link)
  2. ^ Lamport, L. (1977). "Proving the Correctness of Multiprocess Programs". IEEE Transactions on Software Engineering (2): 125–143. CiteSeerX 10.1.1.137.9454. doi:10.1109/TSE.1977.229904.
  3. ^ a b Alpern, B.; Schneider, F. B. (1987). "Recognizing safety and liveness". Distributed Computing. 2 (3): 117. CiteSeerX 10.1.1.20.5470. doi:10.1007/BF01782772.
  4. ^ a b Baier, Christel; Katoen, Joost-Pieter (2008). Principles of Model Checking. MIT Press. p. 104. ISBN 9780262026499.