Estelle es un método de descripción formal de sistemas distribuidos, protocolos de comunicación, basado en un modelo de autómata finito extendido [1] . Desarrollado y estandarizado por ISO (ISO/IEC 9074:1997, ahora retirado) para describir los protocolos del modelo OSI [2] . Define por separado tanto la arquitectura general de un sistema distribuido como el comportamiento de los componentes individuales. Utiliza la sintaxis del lenguaje estándar Pascal [3] .
La especificación, compuesta por módulos, define una estructura jerárquica de componentes no deterministas que interactúan y tienen una relación padre-hijo [3] , en la que el módulo envolvente se denomina "padre" de los módulos descritos en su cuerpo. El módulo envolvente más externo se denomina especificación . Durante la ejecución de la especificación, se pueden crear varias instancias de módulos (inicial o dinámicamente). Desde el punto de vista de los módulos externos, el módulo es una caja negra, cuya interacción se realiza a través de varios puntos de interacción y variables exportadas compartidas [3] .
El encabezado del módulo es la interfaz de comunicación externa del módulo y determina el orden de ejecución en serie o en paralelo de los módulos secundarios. La interfaz de comunicación de un módulo está definida por puntos de interacción , cada uno de los cuales es el final de un canal a través del cual se pueden recibir y transmitir mensajes. Cada punto tiene una cola ( FIFO ) para los mensajes recibidos (la cola puede ser común para varios puntos) [3] [3] .
El cuerpo del módulo describe el comportamiento del componente utilizando un modelo de máquina de estado extendido y describe recursivamente los módulos secundarios [3] [2] . Cada transición de la máquina de estado extendida tiene un conjunto de condiciones adjuntas, bajo las cuales la máquina cambia de estado y (atómicamente) realiza las acciones especificadas [2] .
El comportamiento de todo el sistema se caracteriza por la interacción de instancias de módulos ejecutables. Los módulos secundarios del mismo padre se ejecutan en paralelo, y la ejecución de las instancias del padre tiene prioridad [2] .
La especificación terminada se puede usar para simular el sistema, por ejemplo, usando el kit de herramientas EDT, que permite tanto el modo de simulación aleatoria como el modo definido por el usuario. La especificación se puede utilizar sin modificaciones como una implementación del sistema. Desafortunadamente, la especificación no se puede utilizar para la verificación formal automática o la verificación de modelos , lo cual es una de las desventajas de este enfoque [3] [4] .
Además, está JEstelle, una implementación del formalismo de Estelle en una sintaxis de Java muy limitada (en lugar de Pascal), que le permite utilizar las herramientas de Estelle para comprobar especificaciones estáticas [3] .
Aunque la aplicación de Estelle se limita principalmente a la descripción de sistemas de comunicación distribuidos, se pueden distinguir las siguientes características interesantes de este enfoque [3] :
Las desventajas incluyen [3] :