Estelle je metoda formálního popisu distribuovaných systémů, komunikačních protokolů, založená na rozšířeném modelu konečného automatu [1] . Vyvinuto a standardizováno ISO (ISO/IEC 9074:1997, nyní staženo) k popisu protokolů modelu OSI [2] . Samostatně definuje jak celkovou architekturu distribuovaného systému , tak chování jednotlivých komponent. Používá syntaxi standardního jazyka Pascal [3] .
Specifikace, složená z modulů, definuje hierarchickou strukturu vzájemně se ovlivňujících nedeterministických komponent, které mají vztah rodič-dítě [3] , ve kterém je uzavřený modul nazýván „rodičem“ modulů popsaných v jeho těle. Nejvzdálenější uzavírací modul se nazývá specifikace . Během provádění specifikace lze vytvořit několik instancí modulů (počáteční nebo dynamicky). Z pohledu externích modulů je modul černou skříňkou, s níž interakce probíhá prostřednictvím několika bodů interakce a sdílených exportovaných proměnných [3] .
Záhlaví modulu je externí komunikační rozhraní modulu a určuje sériové nebo paralelní pořadí provádění podřízených modulů. Komunikační rozhraní modulu je definováno interakčními body, z nichž každý je koncem kanálu , přes který lze přijímat a přenášet zprávy. Každý bod má frontu ( FIFO ) pro přijaté zprávy (fronta může být společná pro více bodů) [3] [3] .
Tělo modulu popisuje chování komponenty pomocí modelu rozšířeného stavového stroje a rekurzivně popisuje podřízené moduly [3] [2] . Ke každému přechodu rozšířeného stavového automatu je připojena sada podmínek, za kterých stroj mění stav a (atomicky) provádí zadané akce [2] .
Chování celého systému je charakterizováno interakcí instancí spustitelných modulů. Podřízené moduly stejného rodiče se spouštějí paralelně a spouštění instancí rodiče má přednost [2] .
Hotovou specifikaci lze použít k simulaci systému, například pomocí sady nástrojů EDT, která umožňuje jak režim náhodné simulace, tak režim definovaný uživatelem. Specifikace může být použita bez úprav jako implementace systému. Bohužel specifikaci nelze použít pro automatickou formální verifikaci nebo verifikaci modelů , což je jedna z nevýhod tohoto přístupu [3] [4] .
Kromě toho existuje JEstelle - implementace formalismu Estelle ve velmi omezené syntaxi Java (místo Pascalu), která umožňuje používat nástroje Estelle pro kontrolu statické specifikace [3] .
Přestože je aplikace Estelle omezena především na popis distribuovaných komunikačních systémů, lze rozlišit následující zajímavé rysy tohoto přístupu [3] :
Mezi nevýhody patří [3] :