En la computación distribuida , las propiedades de seguridad requieren informalmente que "algo malo nunca suceda" en un sistema distribuido o algoritmo distribuido . [1] [2] En un sistema de base de datos , la promesa de no devolver nunca datos con campos nulos es un ejemplo de garantía de seguridad. [3] Otro ejemplo es el de la libertad de interbloqueo : nunca debería ocurrir que todos los procesos o un sistema distribuido no puedan continuar porque están esperando la acción de otro proceso. [4]
Las propiedades de seguridad son tipos de propiedades de tiempo lineal estudiadas en el área de verificación de modelos , junto con las propiedades de vivacidad . [4] A diferencia de las propiedades de vida, las propiedades de seguridad pueden violarse mediante una ejecución finita de un sistema distribuido. Todas las propiedades se pueden expresar como la intersección de las propiedades de seguridad y vitalidad . [3]
Referencias
- ^ Rodrigues, Christian Cachin; Rachid Guerraoui; Luís (2010). Introducción a la programación distribuida confiable y segura (2. ed.). Berlín: Springer Berlín. págs. 22-24. ISBN 978-3-642-15259-7.
- ^ Lamport, L. (1977). "Comprobación de la exactitud de los programas multiproceso". Transacciones IEEE sobre ingeniería de software (2): 125–143. CiteSeerX 10.1.1.137.9454 . doi : 10.1109 / TSE.1977.229904 . S2CID 9985552 .
- ^ a b Alpern, B .; Schneider, FB (1987). "Reconociendo la seguridad y la vitalidad". Computación distribuida . 2 (3): 117. CiteSeerX 10.1.1.20.5470 . doi : 10.1007 / BF01782772 . S2CID 9717112 .
- ^ a b Baier, Christel ; Katoen, Joost-Pieter (2008). Principios de la verificación de modelos . Prensa del MIT. pag. 104. ISBN 9780262026499.