Método para la definición y verificación formal de protocolos para aplicaciones de control domótico.

Abstract

Este artículo ofrece un método para la elaboración de protocolos de aplicación de control domóticos, aplicados a un caso de estudio, utilizando herramientas de software libre, PROMELA como su lenguaje de definición formal, y SPIN como su editor, verificador y validador, mediante la simulación.