¿Cómo se puede probar que un protocolo está diseñado correctamente? Estilo de Vida y Elegante

Para los protocolos, hay ciertas cosas que deben ser ciertas para que el protocolo sea correcto.

Primero, debe poder diseñar una máquina de estado completa para el remitente y una máquina de estado distinta para el destinatario.

En segundo lugar, debe poder demostrar que no hay nada que uno pueda enviar al otro que cree un estado indeterminado. Lo hace a través de una red de Petri, que le permite rastrear a través de las máquinas de estado y ver qué se pasan entre sí y cuándo.

Ahora, en realidad no es posible dar a la red de Petri todos los posibles conjuntos de entradas, pero puede usarlo para mostrar que los ejemplos válidos y en mayúsculas y minúsculas se procesan correctamente y que todos los datos erróneos que ingresa están atrapados correctamente sin tener que Cualquier efecto residual o efectos secundarios. Esas son las situaciones que son difíciles de depurar, porque el error que eventualmente surgirá surgirá debido a un error de estado acumulativo y no debido a la entrada en la que falló. En realidad, ver el cambio de estado con cada operación individual es laborioso, pero si desea la corrección, tendrá que pagarlo en las células cerebrales.

Ahora tiene un sistema donde sabe que las interacciones funcionan básicamente. Puede crear conexiones, transmitir datos correctamente, atrapar errores correctamente y cerrar conexiones. Eso es bueno. Eso significa que los problemas relacionados con el tiempo pueden dejarse de lado por un momento, para que podamos centrarnos solo en la lógica.

Tenemos que hacer esto porque Z no tiene concepto del tiempo. Lo cual es un dolor. Z es una lógica establecida para el masoquista, o una forma de programar usando una lógica formal demostrable.

El esquema AZ consiste en primer lugar en una precondición que debe ser verdadera al ingresar a ese esquema. Si no es cierto, el esquema no es válido. Luego consiste en una serie de declaraciones en lógica de predicados que se aplican a conjuntos completos de objetos. Finalmente, tiene la condición posterior que debe ser verdadera al salir del esquema.

Habrá un esquema para cada estado en la máquina de estados, que representa cómo genera la salida de la entrada.

Hay demostradores de teoremas para Z, pero en realidad no es tan malo a mano. Lo que está tratando de mostrar es que no existe una condición posterior de un estado que viole una condición previa para cualquiera de los estados que podrían seguir.

Eso parece bastante simple. Si existe una condición posterior, puede escribir una declaración que diga que existe al menos un objeto para el cual la condición posterior es verdadera y la condición previa es falsa. (Está perfectamente bien tener una situación en la que la condición posterior sea falsa y la condición previa sea verdadera). Si se puede demostrar que la afirmación es paradójica (algo debe ser verdadero y falso para que la afirmación sea verdadera) has establecido que esa transición siempre está bien.

Es agotador hacer esto para cada par de estados conectados, pero si desea una certeza absoluta, hágase un poco de té o café y continúe.

Ahora hemos demostrado que las transiciones de estado son todas válidas (siempre que la comunicación sea válida) y ya hemos demostrado que la comunicación es válida (siempre que las transiciones de estado sean válidas).

Pero el enlace en sí no es necesariamente confiable. Ahora tenemos que demostrar que se puede enviar un paquete válido, luego confundido o perdido en el camino, y manejado correctamente por el otro extremo. En otras palabras, no toda la información no válida se debe a un software no válido.

Ahora tenemos que volver a la red de Petri. Si se pierde un paquete en tránsito, ¿se bloqueará el sistema?

Si se pierde un paquete y se envía uno bueno, ¿el sistema manejará correctamente el paquete que falta? (En un protocolo con pérdida, eso significaría ignorar que faltaba uno. En un protocolo confiable, debe probar que el receptor puede identificar que falta un paquete y recuperarse correctamente).

Si un paquete se encuentra en tránsito, es irrecuperable y no es una entrada válida, ¿el sistema lo descartará correctamente?

Si un paquete se encuentra en tránsito, es recuperable y el protocolo admite la recuperación, ¿se recupera el paquete correctamente?

Si un paquete está confuso en tránsito y ahora es una entrada válida que no debería estar allí, y el protocolo es transaccional, ¿es capaz de detectarlo en algún momento futuro y revertir todas las transacciones hasta el punto de la ruptura?

Primero debe probarlos en la red de Petri porque debe probar que no ingresa un espacio no válido. La red de Petri también simula el tiempo relativo, por lo que puede ver si hay problemas de temporización como resultado de estos problemas. Si está diseñando un protocolo seguro, los ataques de tiempo son un problema. Si está diseñando un protocolo de datos de espacio profundo, no puede presionar un botón de reinicio en un módulo de aterrizaje en Marte. No se puede permitir que la radiación que interfiere con la señal arroje cosas.

Una vez que esté seguro de que no hay estados extraños o rarezas a tiempo, debe verificar el esquema del receptor. Usted sabe que todo está entrando en el estado válido correcto, pero eso no significa que el estado esté haciendo lo correcto y válido.

Para cualquier protocolo, debe saber que si un paquete es confuso e irrecuperable, se identificará y descartará correctamente.

Para un protocolo con pérdida, debe saber que si falta un paquete, el siguiente paquete se procesará como si el paquete anterior hubiera estado presente.

Para un protocolo confiable, debe saber que si faltan N paquetes antes de que llegue el siguiente paquete bueno, la máquina de estado puede identificar que esos N faltan y solicitarlos de alguna manera.

Para un protocolo transaccional, debe saber que si obtiene un paquete confuso pero válido, seguido de otros N paquetes, puede detectar el paquete confuso, hacer una copia de seguridad de todo y luego solicitar que se vuelva a enviar el paquete confuso .

La mayoría de los protocolos no son comprobables o solo lo son para situaciones cuidadosamente seleccionadas. Diseñar un protocolo que sea demostrable en el caso general es factible pero casi nunca se hace. Si alguna vez vemos aviones de línea remota o centros de datos en la luna, tendrá que ser diferente. No puede controlar el entorno ni determinar los parámetros, y no está en condiciones de reiniciar. Tiene que recuperarse el 100% del tiempo, sin importar lo que se le agregue, y los costos (sin importar cómo los calcule) son lo suficientemente grandes como para que sea más barato hacerlo bien la primera vez.