Estelle (limba specifică)

Estelle  este o metodă de descriere formală a sistemelor distribuite, a protocoalelor de comunicație, bazată pe un model extins de automatizare finită [1] . Dezvoltat și standardizat de ISO (ISO/IEC 9074:1997, acum retras) pentru a descrie protocoalele modelului OSI [2] . Definește separat atât arhitectura generală a unui sistem distribuit, cât și comportamentul componentelor individuale. Utilizează sintaxa limbajului standard Pascal [3] .

Descriere

Specificația, compusă din module, definește o structură ierarhică a componentelor nedeterministe care interacționează, care au o relație părinte-copil [3] , în care modulul de încadrare este numit „părinte” modulelor descrise în corpul său. Modulul de închidere cel mai exterior se numește specificație . În timpul execuției specificației, pot fi create mai multe instanțe de module (inițial sau dinamic). Din punctul de vedere al modulelor externe, modulul este o cutie neagră, interacțiunea cu care se realizează prin mai multe puncte de interacțiune și variabile exportate partajate [3] .

Antetul modulului este interfața de comunicare externă a modulului și determină ordinea de execuție în serie sau paralelă a modulelor copil. Interfața de comunicare a unui modul este definită de puncte de interacțiune , fiecare dintre acestea fiind capătul unui canal prin care mesajele pot fi primite și transmise. Fiecare punct are o coadă ( FIFO ) pentru mesajele primite (coada poate fi comună pentru mai multe puncte) [3] [3] .

Corpul modulului descrie comportamentul componentei folosind un model de mașină cu stări extinse și descrie recursiv modulele copil [3] [2] . Fiecare tranziție a mașinii cu stări extinse are atașat un set de condiții, în care mașina își schimbă starea și (atomic) efectuează acțiunile specificate [2] .

Comportamentul întregului sistem este caracterizat de interacțiunea instanțelor modulelor executabile. Modulele copil ale aceluiași părinte se execută în paralel, iar execuția instanțelor părintelui are prioritate [2] .

Instrumente

Specificația finală poate fi utilizată pentru a simula sistemul, de exemplu folosind setul de instrumente EDT, care permite atât modul de simulare aleatoriu, cât și modul definit de utilizator. Specificația poate fi utilizată fără modificare ca implementare a sistemului. Din păcate, specificația nu poate fi utilizată pentru verificarea formală automată sau verificarea modelelor , ceea ce este unul dintre dezavantajele acestei abordări [3] [4] .

În plus, există JEstelle - o implementare a formalismului Estelle într-o sintaxă Java foarte limitată (în loc de Pascal), care vă permite să utilizați instrumentele Estelle pentru verificarea statică a specificațiilor [3] .

Avantaje și dezavantaje

Deși aplicarea lui Estelle se limitează în principal la descrierea sistemelor de comunicații distribuite, se pot distinge următoarele caracteristici interesante ale acestei abordări [3] :

• capacitatea de a amâna deciziile cu privire la o anumită metodă de implementare jucând mai multe opțiuni pe o specificație de bază
• capacitatea de a exprima non-determinismul
• implementarea unui sistem distribuit bazat pe o specificație gata făcută

Dezavantajele includ [3] :

• nu există mecanisme de corectare a erorilor în cerințele de sistem ale utilizatorului, deși specificația poate clarifica unele puncte
• nu oferă metode formale de validare

Note

1. ↑ Okunishnikova, 2000 .
2. ↑ 1 2 3 4 Budkowski, Cavalli, Najm, 1998 .
3. ↑ 1 2 3 4 5 6 7 8 9 10 Habrias, Frappier, 2006 .
4. ↑ Budkowski S. „Estelle Development Toolset”. Computer Networks and ISDN Systems 25:63-82, 1992

Literatură

• Henri Habrias, Marc Frappier. Capitolul 11 ​​Estelle // Metode de specificare software. - John Wiley & Sons, 2006. - 418 p. — ISBN 978-1-905-20934-7 .
• Okunishnikova E. V. Modelarea construcțiilor dinamice ale limbajului Estelle folosind rețele Petri colorate  : preprint. - Novosibirsk: Institutul de Sisteme Informatice. A. P. Ershova SO RAN, 2000.  (link inaccesibil)
• ISO/IEC Tehnologia informației - Interconectarea sistemelor deschise - Estelle: O tehnică de descriere formală bazată pe un model de tranziție de stare extinsă. ISO/IEC 9074:1997 , Organizația Internațională pentru Standardizare, Geneva, Elveția, 1997
• Budkowski, S. și Cavalli, A. și Najm, E. Un editor de reprezentare grafică și prototip pentru tehnica de descriere formală Estelle // Tehnici de descriere formală și specificarea protocolului, testare și verificare. - Springer, 1998. - 467 p. — ISBN 9780412847608 .