Propiedades de seguridad y habitabilidad

Las propiedades de la ejecución de un programa informático —en particular para sistemas concurrentes y distribuidos— se han formulado durante mucho tiempo mediante la asignación de propiedades de seguridad ("no ocurren cosas malas") y propiedades de vivacidad ("ocurren cosas buenas"). ^{[ 1 ]}

Un programa es totalmente correcto con respecto a una condición previa.${\displaystyle P}$y postacondicionamiento${\displaystyle Q}$si alguna ejecución comenzó en un estado que satisface${\displaystyle P}$termina en un estado que satisface${\displaystyle Q}$. La corrección total es una conjunción de una propiedad de seguridad y una propiedad de vivacidad: ^{[ 2 ]}

• La propiedad de seguridad prohíbe estas "cosas malas": ejecuciones que comienzan en un estado que satisface${\displaystyle P}$y terminan en un estado final que no satisface${\displaystyle Q}$Para un programa${\displaystyle C}$Esta propiedad de seguridad se suele escribir utilizando la tripleta de Hoare.${\displaystyle \{P\}C\{Q\}}$.
• La propiedad de vivacidad, lo "bueno", es esa ejecución que comienza en un estado satisfactorio${\displaystyle P}$finaliza.

Nótese que un hecho negativo es discreto, ^{[ 3 ]} puesto que ocurre en un lugar específico durante la ejecución. Un hecho positivo no tiene por qué ser discreto, pero la propiedad de vivacidad de la terminación sí lo es.

Las definiciones formales que finalmente se propusieron para las propiedades de seguridad ^{[ 4 ]} y las propiedades de vivacidad ^{[ 5 ]} demostraron que esta descomposición no solo es intuitivamente atractiva, sino también completa: todas las propiedades de una ejecución son una conjunción de propiedades de seguridad y vivacidad. ^{[ 5 ]} Además, realizar la descomposición puede ser útil, porque las definiciones formales permiten demostrar que deben usarse métodos diferentes para verificar las propiedades de seguridad y para verificar las propiedades de vivacidad. ^{[ 6 ] [ 7 ]}

Una propiedad de seguridad prohíbe que ocurran cosas malas discretas durante una ejecución. ^{[ 1 ]} Una propiedad de seguridad caracteriza así lo que está permitido al indicar lo que está prohibido. El requisito de que la cosa mala sea discreta significa que una cosa mala que ocurra durante la ejecución necesariamente ocurre en algún punto identificable. ^{[ 5 ]}

Ejemplos de un elemento negativo discreto que podría usarse para definir una propiedad de seguridad incluyen: ^{[ 5 ]}

• Una ejecución que comienza en un estado que satisface una precondición dada termina, pero el estado final no satisface la postcondición requerida;
• Una ejecución de dos procesos concurrentes, donde el programa cuenta las instrucciones que designan ambos procesos dentro de una sección crítica ;
• Una ejecución de dos procesos concurrentes donde cada proceso está esperando a que el otro cambie de estado (conocido como interbloqueo ).

La ejecución de un programa puede describirse formalmente mediante la secuencia infinita de estados del programa que resultan a medida que avanza la ejecución, donde el último estado de un programa que finaliza se repite infinitamente. Para un programa de interés, sea:${\displaystyle S}$denota el conjunto de posibles estados del programa,${\displaystyle S^{*}}$denotamos el conjunto de secuencias finitas de estados del programa, y${\displaystyle S^{\omega }}$denotan el conjunto de secuencias infinitas de estados del programa. La relación${\displaystyle \sigma \leq \tau }$se aplica a secuencias${\displaystyle \sigma }$y${\displaystyle \tau }$si y solo si${\displaystyle \sigma }$es un prefijo de${\displaystyle \tau }$o${\displaystyle \sigma }$igual${\displaystyle \tau }$. ^{[ 5 ]}

Una propiedad de un programa es el conjunto de ejecuciones permitidas.

La característica esencial de una propiedad de seguridad${\displaystyle SP}$es: Si alguna ejecución${\displaystyle \sigma }$no satisface${\displaystyle SP}$entonces el aspecto negativo definitorio para esa propiedad de seguridad ocurre en algún momento${\displaystyle \sigma }$. Observe que después de algo tan malo , si la ejecución posterior resulta en una ejecución ${\displaystyle \sigma ^{\prime }}$, entonces${\displaystyle \sigma ^{\prime }}$tampoco satisface${\displaystyle SP}$, ya que lo malo en${\displaystyle \sigma }$también ocurre en${\displaystyle \sigma ^{\prime }}$. Tomamos esta inferencia sobre la irremediabilidad de las cosas malas como la característica definitoria para${\displaystyle SP}$ser una propiedad de seguridad. Formalizar esto en lógica de predicados da una definición formal para${\displaystyle SP}$ser una propiedad de seguridad. ^{[ 5 ]}

${\displaystyle \forall \sigma \in S^{\omega }:\sigma \notin SP\implies (\exists \beta \leq \sigma$ :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))}

Esta definición formal de propiedades de seguridad implica que si una ejecución${\displaystyle \sigma }$ satisface una propiedad de seguridad${\displaystyle SP}$entonces cada prefijo de${\displaystyle \sigma }$(con el último estado repetido) también satisface${\displaystyle SP}$.

Una propiedad de vivacidad prescribe cosas buenas para cada ejecución o, equivalentemente, describe algo que debe suceder durante una ejecución. ^{[ 1 ]} La cosa buena no tiene por qué ser discreta; podría implicar un número infinito de pasos. Ejemplos de una cosa buena utilizada para definir una propiedad de vivacidad incluyen: ^{[ 5 ]}

• Finalización de una ejecución que se ha iniciado en un estado adecuado;
• No finalización de una ejecución que se ha iniciado en un estado adecuado;
• Acceso garantizado a una sección crítica siempre que se intente entrar;
• Acceso equitativo a un recurso en presencia de controversia.

Lo bueno en el primer ejemplo es discreto, pero no en los demás.

Generar una respuesta dentro de un límite de tiempo real especificado es una propiedad de seguridad, no de vivacidad. Esto se debe a que se prohíbe un problema concreto : una ejecución parcial que alcanza un estado en el que aún no se ha generado la respuesta y el valor del reloj (una variable de estado) excede el límite. La ausencia de interbloqueos es una propiedad de seguridad: el problema reside en un interbloqueo (que es un fenómeno discreto).

En la mayoría de los casos, saber que un programa finalmente realiza alguna acción positiva no es suficiente; lo que necesitamos es saber que la realiza dentro de un número determinado de pasos o antes de una fecha límite. Una propiedad que establece un límite específico para dicha acción positiva es una propiedad de seguridad (como se mencionó anteriormente), mientras que la propiedad más débil que simplemente afirma que existe dicho límite es una propiedad de vivacidad. Demostrar una propiedad de vivacidad probablemente sea más sencillo que demostrar la propiedad de seguridad, ya que no requiere el nivel de detalle necesario para demostrar la propiedad de seguridad.

A diferencia de una propiedad de seguridad, una propiedad de vivacidad${\displaystyle LP}$no se puede descartar ningún prefijo finito ${\displaystyle \alpha \in S^{*}}$^{[ 8 ]} de una ejecución (ya que tal una${\displaystyle \alpha }$sería algo "malo" y, por lo tanto, definiría una propiedad de seguridad). Eso lleva a definir una propiedad de vivacidad.${\displaystyle LP}$ser una propiedad que no excluya ningún prefijo finito. ^{[ 5 ]}

${\displaystyle \forall \alpha \in S^{*}:(\exists \tau \in S^{\omega }:\alpha \tau \in LP)}$

Esta definición no restringe algo bueno a ser discreto; lo bueno puede involucrar todo${\displaystyle \tau }$, que es una ejecución de duración infinita.

Lamport utilizó los términos propiedad de seguridad y propiedad de vivacidad en su artículo de 1977 ^{[ 1 ]} sobre la demostración de la corrección de programas multiproceso (concurrentes) . Tomó prestados los términos de la teoría de redes de Petri , que utilizaba los términos vivacidad y acotación para describir cómo podía evolucionar la asignación de los "tokens" de una red de Petri a sus "lugares"; la seguridad de las redes de Petri era una forma específica de acotación . Posteriormente, Lamport desarrolló una definición formal de seguridad para un curso corto de la OTAN sobre sistemas distribuidos en Múnich. ^{[ 9 ]} Esta definición asumía que las propiedades son invariantes bajo tartamudeo . La definición formal de seguridad mencionada anteriormente aparece en un artículo de Alpern y Schneider; ^{[ 5 ]} la conexión entre las dos formalizaciones de las propiedades de seguridad aparece en un artículo de Alpern, Demers y Schneider. ^{[ 10 ]}

Alpern y Schneider ^{[ 5 ]} dan la definición formal de vivacidad, acompañada de una demostración de que todas las propiedades pueden construirse utilizando propiedades de seguridad y propiedades de vivacidad. Esa demostración se inspiró en la idea de Gordon Plotkin de que las propiedades de seguridad corresponden a conjuntos cerrados y las propiedades de vivacidad corresponden a conjuntos densos en una topología natural en el conjunto${\displaystyle S^{\omega }}$de secuencias infinitas de estados del programa. ^{[ 11 ]} Posteriormente, Alpern y Schneider ^{[ 12 ]} no solo dieron una caracterización de autómata de Büchi para las definiciones formales de propiedades de seguridad y propiedades de vivacidad, sino que utilizaron estas formulaciones de autómatas para mostrar que la verificación de las propiedades de seguridad requeriría un invariante y la verificación de las propiedades de vivacidad requeriría un argumento de buena fundamentación . La correspondencia entre el tipo de propiedad (seguridad vs. vivacidad) con el tipo de prueba (invariancia vs. buena fundamentación) fue un argumento fuerte de que la descomposición de las propiedades en seguridad y vivacidad (en contraposición a alguna otra partición) era útil: conocer el tipo de propiedad a probar dictaba el tipo de prueba que se requería.