Safety Property

From Handwiki

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, if a safety property is violated there is always a finite execution that shows the violation. All properties can be expressed as the intersection of safety and liveness properties.[3]

See also

  • Safety and liveness properties

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. 
  2. Lamport, L. (1977). "Proving the Correctness of Multiprocess Programs". IEEE Transactions on Software Engineering (2): 125–143. doi:10.1109/TSE.1977.229904. 
  3. 3.0 3.1 Alpern, B.; Schneider, F. B. (1987). "Recognizing safety and liveness". Distributed Computing 2 (3): 117. doi:10.1007/BF01782772. 
  4. 4.0 4.1 Baier, Christel; Katoen, Joost-Pieter (2008). Principles of Model Checking. MIT Press. p. 104. ISBN 9780262026499. 



Retrieved from "https://handwiki.org/wiki/index.php?title=Safety_property&oldid=2239064"

Categories: [Distributed computing]


Download as ZWI file | Last modified: 12/11/2022 13:54:09 | 7 views
☰ Source: https://handwiki.org/wiki/Safety_property | License: CC BY-SA 3.0

ZWI signed:
  Encycloreader by the Knowledge Standards Foundation (KSF) ✓[what is this?]