Estelle er en metode til formel beskrivelse af distribuerede systemer, kommunikationsprotokoller, baseret på en udvidet finite automatmodel [ 1] . Udviklet og standardiseret af ISO (ISO/IEC 9074:1997, nu trukket tilbage) til at beskrive protokollerne i OSI-modellen [2] . Definerer separat både den overordnede arkitektur af et distribueret system og adfærden af individuelle komponenter. Bruger syntaksen for standardsproget Pascal [3] .
Specifikationen, der er sammensat af moduler, definerer en hierarkisk struktur af interagerende ikke-deterministiske komponenter, der har et forældre-barn-forhold [3] , hvor det omsluttende modul kaldes "forælderen" af de moduler, der er beskrevet i dens krop. Det yderste omsluttende modul kaldes specifikationen . Under udførelsen af specifikationen kan der oprettes flere forekomster af moduler (initielt eller dynamisk). Fra eksterne modulers synspunkt er modulet en sort boks, som interaktion med hvilken udføres gennem flere interaktionspunkter og delte eksporterede variabler [3] .
Moduloverskriften er modulets eksterne kommunikationsgrænseflade og bestemmer den serielle eller parallelle udførelsesrækkefølge for underordnede moduler. Et moduls kommunikationsgrænseflade er defineret af interaktionspunkter , som hver er slutningen af en kanal, over hvilken meddelelser kan modtages og transmitteres. Hvert punkt har en kø ( FIFO ) for modtagne beskeder (køen kan være fælles for flere punkter) [3] [3] .
Modulets krop beskriver opførselen af komponenten ved hjælp af en udvidet tilstandsmaskinemodel og beskriver rekursivt de underordnede moduler [3] [2] . Hver overgang af den udvidede tilstandsmaskine har et sæt betingelser knyttet til sig, under hvilke maskinen skifter tilstand og (atomisk) udfører de specificerede handlinger [2] .
Hele systemets opførsel er karakteriseret ved samspillet mellem forekomster af eksekverbare moduler. Underordnede moduler af samme forælder udføres parallelt, og udførelse af forekomster af forælderen har forrang [2] .
Den færdige specifikation kan bruges til at simulere systemet, for eksempel ved hjælp af EDT-værktøjssættet, som tillader både tilfældig simuleringstilstand og brugerdefineret tilstand. Specifikationen kan bruges uden ændringer som en implementering af systemet. Desværre kan specifikationen ikke bruges til automatisk formel verifikation eller verifikation af modeller , hvilket er en af ulemperne ved denne tilgang [3] [4] .
Derudover er der JEstelle - en implementering af Estelle-formalismen i en meget begrænset Java-syntaks (i stedet for Pascal), som giver dig mulighed for at bruge Estelle-værktøjer til statisk specifikationskontrol [3] .
Selvom anvendelsen af Estelle hovedsageligt er begrænset til beskrivelsen af distribuerede kommunikationssystemer, kan følgende interessante træk ved denne tilgang skelnes [3] :
Ulemperne omfatter [3] :