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.