Metodología para la definición y verificación formal de protocolos de control domóticos

Resumen

La sociedad en los últimos años ha marcado un paso acelerado en su informatización, la ingeniería de protocolos ha quedado en un lado oscuro y selectivo, mayoritariamente en el sector privado. Basado en el estudio de la evolución histórica y actual de esta rama utilizando dos métodos de investigación teóricos, el analítico-sintético y la moderación para la recopilación y análisis del estado del arte de este amplio tema, que abarca desde los lenguajes de especificación formal, pasando por tecnologías de modelación, hasta los lenguajes y herramientas de verificación, validación y simulación de protocolos, así como el empírico-experimental, permitiendo el aprendizaje y toma de experiencias prácticas en el uso de herramientas adecuadas para verificación y validación. Por lo tanto este artículo ofrece una metodología para la elaboración de protocolos de aplicación de control domóticos, utilizando herramientas de software libre, PROMELA como su lenguaje de definición formal, SPIN como su editor, verificador y validador mediante la simulación.

Palabras Clave: Domótica, Ingeniería de Protocolos, Metodología, PROMELA, SPIN, Software Libre, Verificación, Validación

Methodology for the definition and formal verification of protocols automation applications

Abstract

The company in recent years has marked a step accelerated computerization, protocol engineering has reached a dark and selective side, mostly in the private sector. Based on the study of historical and current developments in this branch using two methods of theoretical research, analytic-synthetic and moderation for the collection and analysis of the state of the art of this broad topic, ranging from the formal specification languages, through modeling technologies, languages ??and tools to the verification, validation and simulation of protocols and empirical-experimental, allowing learning and practical experiences in making the use of appropriate tools for verification and validation. Therefore this article provides a methodology for the development of protocols for implementing automation control, using free software tools, language PROMELA as its formal definition, SPIN as its editor, verifier and validator using simulation.

Keywords: Automation, Engineering Protocols, Methodology, PROMELA, SPIN, Free Software, Verification, Validation.

Introducción

El desarrollo acelerado de la producción de software y cada día más orientado a servicios, con el paradigma cliente–servidor, ha hecho que la ingeniería de protocolos se desarrolle, aunque no siempre se realice un trabajo en cada ocasión que se transmitan datos, provocado por muchos factores.

Uno de estos factores es el desconocimiento de los desarrolladores, de la existencia de métodos de descripción formal y verificación de protocolos de red, que ayudan tener corrección, robustez y rendimiento al protocolo de comunicación que se desea aplicar. Por otra parte, en ocasiones, teniendo este conocimiento, se hace difícil asegurar estos aspectos, debido a que no se cuenta con las herramientas automatizadas correspondientes a estos métodos ya que están bajo licencias privativas y se carece de una metodología adecuada que guie el flujo de trabajo para lograr los objetivos deseados.

El objetivo que persigue este artículo es, desarrollar una metodología para la definición y verificación formal de protocolos para aplicaciones de control domóticos con métodos de descripción formal disponibles y herramientas de verificación, validación y simulación bajo licencia libre.

Metodología Computacional

Para el desarrollo de la investigación se divide en las siguientes tareas:

• 1. Análisis bibliográfico para establecer el estado del arte y perfilar el trabajo.

• 2. Determinar el modelo de ingeniería de protocolo a usar.

• 3. Análisis de los resultados y las conclusiones.

• 4. Escritura de los resultados.

El estado del arte para el desarrollo de una metodología de ingeniería de protocolos es muy amplio, cabe investigar, de las técnicas de descripción formal donde el uso de lenguajes formales de especificación permite realizar análisis y simulaciones de posibles soluciones alternativas a un determinado sistema, pudiendo comprobar cuál de ellas es la más adecuada y efectuar una selección durante la etapa de diseño que supondrá un importante ahorro en tiempo y costos, también de las tecnologías de modelación que constituyen un paso importante en el desarrollo del protocolo, constituyendo el primer paso de abstracción de los requerimientos de usuario deseados para ser llevados al análisis con herramientas de cómputo. La verificación es un rol importante en la vida de cualquier sistema, por lo que en la ingeniería de protocolo no escapa su presencia en sus metodologías. Haciendo uso de herramientas-software se realiza este paso, para verificar si los requisitos de usuarios fueron modelados correctamente y si estos modelos fueron representados con una definición formal correcta. Varios son los software que se utilizan para este paso, pero la gran mayoría está en manos de instituciones privadas y existen algunas soluciones libres que permiten llevar a cabo este proceso.

Preguntas de la Investigación

Las preguntas de la investigación constituyen puntos de arranque para el desarrollo de la investigación y son las siguientes:

• 1. ¿Es posible determinar la metodología para la definición y verificación formal de protocolos domóticos?

• 2. ¿Será posible encontrar una herramienta de software libre para la modelación, verificación, validación y simulación necesaria para la metodología?

El resultado de la investigación arroja la carencia de metodologías para la definición y verificación formal de protocolos, aunque no faltan los resultados de fuentes sobre la investigación de temas en la verificación, o la validación de protocolos de forma separada, donde la gran mayoría de estas que usan software propietarios para la validación y simulación están patrocinadas por compañías interesadas en la investigación que realizan.

La necesidad de contar con una metodología de ingeniería de protocolos con herramientas de software libre para el uso académico mayoritariamente y garantizar soberanía tecnología hace que la unificación del estudio de estas fuentes hizo posible el resultado alcanzado como se desarrolla en este artículo.

Técnicas de descripción formal

Las técnicas de descripción formal son una herramienta de uso común para los equipos de desarrollo de sistemas durante su ciclo de vida, para ello deben contar con reglas bien definidas para que los distintos grupos que interactúan en el desarrollo puedan realizar especificaciones con la misma técnica de descripción formal y exista compatibilidad entre ellas.

Se adoptó el término FDT como siglas en inglés (Formal Description Techniques), para referirse a los lenguajes y métodos formales que se iban a normalizar. Aunque el término FDT actualmente se utiliza para cualquier lenguaje o método que tenga una base formal, su uso adecuado es para referirse a las técnicas formales normalizadas por la ISO y el CCITT.

La ISO desarrolló dos categorías:

• Métodos formales basados en autómatas de estado finito (ESTELLE).

• Métodos formales basados en métodos algebraicos (LOTOS).

Encargándose CCITT de realizar normas en el campo de las telecomunicaciones.

Desarrolladas con la finalidad de que sistemas, equipos y protocolos o normas:

• No presenten ambigüedad, sean claras y concisas.

• Sean completas.

• Sean consistentes con sí mismas o en relación con otras.

• Sean manejables teniendo una fácil legibilidad e interpretación.

• Que las realizaciones se ajusten a ellas.

De esta forma las especificaciones son completas con una única interpretación universal.

Con el uso de las FDTs se descubren errores, ambigüedades e inconsistencias en la especificación que se está desarrollando; también ayuda a realizar un estudio estructurado del problema que se quiere resolver, lo que supone una mejora en la etapa de planteamiento de su resolución. (ISO/IEC 9074, 1989)

Resultados y discusión

El diseño y estudio de protocolos de comunicación comprende varias etapas, entre las que se encuentra requisitos de usuario, su análisis cuantitativo y cualitativo, su realización práctica y documentación. El primer aspecto, la definición del protocolo es de suma importancia, ya que es el punto de partida de un largo proceso que se describe en la Figura 1.

Figura 1. Metodología de desarrollo.

Requerimientos de usuario

Los requerimientos del protocolo deseado se conforman con el conjunto de necesidades que establece la comunicación deseada, se describen con un lenguaje natural. Desde 1979, (Hoffmann, 1979) le confiere gran importancia a esta parte, aunque no deja de introducir ambigüedades propias del leguaje humano, con el consiguiente riesgo de interpretaciones distintas por parte de las personas encargadas de implementar el protocolo. Por lo que diversos autores han definido métodos formales para la definición de protocolos que por otra parte, se prestan mejor que el lenguaje escrito, para el estudio de sus características y basados en los siguientes aspectos:

• Nivel del modelo de referencia en el cual trabajara

• Forma de delimitación de unidad de datos (trama, paquete, celda, etc)

• Si debe tener capacidad de multidifusión, broadcast o solamente punto a punto.

• Si va a tener direccionado para encaminamiento final o multiplexación correspondientes al nivel del modelo de referencia en el cual trabaja.

• Si va a tener orientación a conexión o no, o ambas posibilidades.

• Para participar en conmutación, repetición o punto a punto.

• Si tiene direccionado, su alcance y procesamiento para accesar la entidad final.

• Longitud de la carga útil. Si será fija o variable.

• Si tendrá detección y corrección de errores, y si se aplicaran mecanismos de repetición automática sobre la base de confirmaciones y almacenamiento en ventana deslizantes.

• Si se aplicaran mecanismos de control de errores hacia delante FEC.

• Si va a tener control de flujo o de congestión.

• Capacidad de recuperación frente a fallas.

Requisitos de la especificación formal

Se realiza un análisis de los requerimientos de usuarios para hacer una transformación a los requisitos necesarios de la herramienta de modelación, paso importante para lograr una correcta interpretación y por consiguiente una modelación lo más exacta posible a lo deseado.

Modelación

En esta etapa se lleva todo el análisis realizado en las etapas anteriores a un modelo usando la tecnología adecuada según las características del protocolo. Constituye un paso importante en el desarrollo del protocolo, siendo el primer paso de abstracción de los requerimientos de usuario deseados para ser llevados al análisis con herramientas de cómputo.

Máquina de Estado Finito: Es un modelo abstracto para la manipulación de símbolos, útiles para saber si una cadena pertenece a un lenguaje o pueden generar otro conjunto de símbolos como resultado. Los Autómatas se caracterizan por tener un Estado inicial, reciben una cadena de símbolos, cambian de estado por cada elemento leído o pueden permanecer en el mismo estado. También tienen un conjunto de Estados Finales o Aceptables que indican si una cadena pertenece al lenguaje al final de una lectura. (V. Cerf)

Redes de Petri: Representan una alternativa para modelar sistemas, sus características hacen que, para algunos problemas las redes de Petri funcionen de una manera natural con ella podemos modelar el comportamiento y la estructura de un sistema, y llevar el modelo a condiciones límite, que en un sistema real son difíciles de lograr o muy costosas. Las PN ofrecen una forma de expresar procesos que requieren sincronía. Y quizás lo más importante es que las PN pueden ser analizadas de manera formal y obtener información del comportamiento dinámico del sistema modelado. (Bautista, 2005)

Definición Formal

Esta etapa es cuando comienza a cambiar el lenguaje utilizado, pasando del lenguaje natural a un lenguaje de máquina. PROMELA es un lenguaje que permite escribir en código el resultado de la etapa de modelación utilizando también SPIN como editor.

PROMELA es una extensión de un lenguaje llamado ARGOS, que fue desarrollado en 1983 para la validación de protocolos. La validación de programas está definida directamente en términos de tres tipos de objetos en específico y estos son:

• Procesos.

• Canales de Mensajes.

• Variables de Estados.

Todos los procesos se definen como objetos globales, y los cuales pueden contener variables y/o canales de comunicación, los cuales representan datos que pueden ser locales o globales a un proceso. Las variables en PROMELA son usadas para almacenar ya sea información global acerca del sistema como un todo, o como información que es local para un proceso en específico, dependiendo de dónde se haya localizada la declaración de la variable. (Fernández, 2008)

Verificación/Validación

Al finalizar la especificación formal queda listo para la Verificación y Validación.

La metodología descrita debe permitir:

• Escribir especificaciones sin ambigüedad, claras, precisas y concisas.

• Analizar y corregir en su plenitud una especificación.

• Determinar si un diseño cumple con determinada especificación.

• Utilizar herramientas para crear, mantener, analizar y simular especificaciones. ( Salinas, 2008)

Para validar y verificar el diseño realizado del protocolo es preciso llevar los requisitos de la especificación formal a un lenguaje que sea capaz de entender la computadora, siendo capaz así de lograr el proceso de verificación y simulación automática del protocolo.

Con la validación se persiguen varios objetivos:

• Corrección: la garantía de mostrar los comportamientos previstos en cualquier situación específica.

• Robustez: la propiedad de ser capaz de trabajar correctamente en condiciones anormales.

• Rendimiento: La capacidad de lograr el ancho de banda disponible en el medio físico.

Con la realización de la verificación y validación se persigue:

• Reducir la complejidad.

• Eliminar la ambigüedad.

• Preparar protocolo estructurado. ( Venkataram, 2008)

Conclusiones

El resultado alcanzado en este trabajo constituye una metodología para el desarrollo de protocolos de aplicación de control domótico. A partir de los requerimientos demandados al protocolo, se estudian las vías de su modelación teniendo en cuenta los requisitos de especificación formal se determina la tecnología de modelación adecuada, posteriormente se realiza la definición formal a partir del lenguaje PROMELA, y su verificación con la herramienta SPIN.

Las herramientas utilizadas en la metodología para la definición y verificación formal de protocolos de control domóticos trabajan bajo la licencia GNU/GPL o sea software libre lo que constituye un paso de avance para la soberanía tecnológica de nuestro país.

Referencias

• 1. ISO/IEC 9074, Information processing systems, Open System Interconnection, ESTELLE: A formal description technique based on an Extended Transition Model, 1989.

• 2. Hoffmann, M. G. Técnicas para la Descripción Formal y Verificación de protocolos, 1979.

• 3. V. Cerf, How the Internet came to be: the birth of the ARPANET disponible en http://www.netvalley.com/archives_mirror/cerf-how-inet.txt

• 4. Bautista Cuéllar, Ricardo V. Domótica. Especificaciones técnicas y estándares.2005.

• 5. Fernández Molina, Pablo. Diseño de nodos inteligentes para instalaciones domóticas basadas en bus. 2008.

• 6. Salinas, R. G. Especificación del Protocolo FlexRay utilizando un lenguaje de descripción formal, Universidad Tecnológica de la Mixteca: 146, Julio 2008.

• 7. Venkataram, P. P. Protocol Verification Validation. Departament of Electrical Communication Engeneering. Bangalore, IndianInstitute of Science: 33, 2008.

Autor:

Arian Trujillo Díaz 1

1 Universidad de Pinar del Río "Hermanos Saíz Montes de Oca". Calle Martí Final Pinar del Río.