[ad_1]
Los miembros pueden Descargue este artículo en formato PDF.
Lo que vas a aprender:
- Los pasos simples para desarrollar una especificación de mensaje complejo con RecordFlux.
- Cómo implementar esta especificación en el código de la aplicación Ada/SPARK.
Traducir la especificación de un mensaje del papel al código puede resultar complicado y propenso a errores. En el mejor de los casos, todos los aspectos de la especificación del mensaje se implementan en código de programa, alojados en estructuras, con potencialmente miles de líneas de codificación defensiva y/o manejo de excepciones para detectar posibles errores. Cada mensaje recibido puede volverse complejo si se requieren condiciones, declaraciones de casos o subprogramas para verificar la validez del mensaje.
Este proceso no sólo es engorroso para el desarrollador de la aplicación, sino que también dificulta o casi imposibilita el mantenimiento de la aplicación. Y las pruebas y la depuración… ¡peor aún! Buscar entre miles de líneas de código y condiciones es un proceso que requiere mucho tiempo. Los errores de filtración también podrían exponer toda la aplicación a graves problemas de seguridad (por ejemplo, ataques cibernéticos).
Ingrese a RecordFlux. RecordFlux es una poderosa herramienta para implementar especificaciones de mensajes seguros. El poder de esta herramienta radica en su capacidad para generar código SPARK verificable a partir de una especificación y simplificar el proceso de traducción de un protocolo del papel al código. ¿Cómo se aplica esto al desarrollador de aplicaciones?
La especificación del mensaje está aislada en un archivo RecordFlux. Usando el lenguaje RecordFlux, los desarrolladores pueden definir estrictamente el flujo de mensajes, restricciones, límites, etc. – todas las cosas que, si se integran en una aplicación normal, podrían ocupar miles de líneas en prácticas de codificación defensiva. El código SPARK generado a partir del archivo RecordFlux, cuando se implementa en código, garantiza que la implementación del mensaje en la aplicación sea demostrable y segura.
En este artículo, recorreremos el proceso inicial de implementación de una especificación RecordFlux para un protocolo del mundo real. También describimos el proceso de ejecutar el código generado por RecordFlux en un conjunto simple de aplicaciones cliente/servidor. Esto proporciona una imagen completa de cómo se puede transferir algo de la «descripción del protocolo» a la «realidad de la aplicación».
El protocolo (y el alcance de la muestra)
El protocolo que implementé para este ejemplo es el Protocolo de control de congestión de datagramas (DCCP). Aquí solo describiré brevemente el protocolo ya que el foco de esta discusión está en RecordFlux y no en los detalles de DCCP.
DCCP es un protocolo de capa de transporte que proporciona un medio confiable para negociar conexiones (desde la conexión hasta el cierre) y proporciona mecanismos integrados de control de congestión. Funciona de manera similar a TCP, pero no garantiza que los mensajes se entreguen en el orden correcto.
DCCP no es un protocolo ampliamente utilizado, pero puede brindar beneficios para transmisión de medios, juegos, telemetría y otras aplicaciones donde la sincronización (baja latencia) y la confiabilidad son importantes. RFC 4340 describe la estructura básica del protocolo, que consta de un encabezado DCCP seguido de un área de datos de aplicación. (Figura 1).
[ad_2]