Proprietatea de corectitudine a reţelelor flux de lucru

PROPRIETATEA DE CORECTITUDINE A REŢELELOR FLUX DE LUCRU
ŢIŢCHIEV Inga

Institutul de Matematică şi Informatică al AŞM

Universitatea de Stat din Tiraspol
Recenzent: BRAICOV Andrei, dr.
Cuvinte cheie: reţele flux de lucru, corectitudine, comunicare sincronă, comunicare asincronă
Obiectivul acestui articol constă în studierea şi stabilirea relaţiilor de legătură între proprietatea de corectitudine ale reţelelor petri flux de lucru şi automatelor cu un număr finit de stări [2]. Corectitudinea este o proprietate care poate fi aplicată la descoperirea comportamentului arhitecturilor bazate pe oferirea serviciilor [3]. În dependenţă de modelul de comunicare (sincron/asincron) în oferirea serviciilor se pot obţine diferite rezultate.

Reţelele Petri [1] reprezintă un formalism de verificare a proprietăţilor sistemelor distribuite. Reţelele flux de lucru sunt o extensie a reţelelor petri ordinare, care posedă două stări suplimentare, starea iniţială – i şi starea finală o. Reţelele flux de lucru se bazează pe studierea cazurilor ce pot fi generate de clienţi externi sau care sunt generate din interior.

Proprietatea de corectitudine implică faptul că din orice marcare accesibilă se poate ajunge în marcarea finală o. În acest mod este garantată execuţia cu succes a unui caz particular. În afară de aceasta o altă cerinţă pentru îndeplinirea proprietăţii de corectitudine este acoperirea tuturor tranziţiilor cu o secvenţă de execuţie a acestora corectă.

Dacă ne referim la comportamentul arhitecturilor bazate pe oferirea serviciilor, atunci când două servicii care interacţionează sunt corecte, aceasta garantează faptul că interacţiunea se va încheia cu succes, adică nu vom avea blocaje. În studierea interacţiunii a două servicii este esenţială investigarea ipotezelor celor două servicii. Astfel la comunicarea sincronă dacă un mesaj este trimis înaintea altui mesaj, atunci ele trebuie să fie recepţionate în aceeaşi ordine. La comunicarea asincronă ordinea recepţionării mesajelor poate să nu coincidă cu ordinea trimiterii lor. Pentru modelarea acestor tipuri de comunicări se vor utiliza construcţiile XOR-split, XOR-join, AND-split, AND-join. Utilizarea construcţiilor XOR nu garantează respectarea proprietăţii de corectitudine deoarece daca intenţionăm să trimitem un al doilea mesaj către destinatar, atunci aceasta nu este capabil să îl gestioneze. Utilizarea construcţiei AND pentru modelul de comunicare asincron garantează corectitudinea, deoarece ordinea recepţionării mesajelor este irelevantă, însă pentru modelul de comunicare sincronă se poate întâmpla ca ordinea recepţionării mesajelor să nu fie cea dorită. Pentru a verifica aceeaşi proprietate vom utiliza şi reprezentarea modelelor de comunicare prin automate finite în care informaţia despre direcţia schimbului de date este stocată în etichetele tranziţiilor şi anume e#d#mes, unde e specifică expeditorul, d destinatarul, mes mesajul transmis. Orice flux de lucru are atribuit un nume de rol care se utilizeaă pentru identificarea expeditorului şi destinatarului. Două fluxuri de lucru se potrivesc dacă au roluri diferite şi interacţionează cu succes, adică toate mesajele trimise de expeditor sunt relevante, iar toate mesajele primite de către destinatar sunt opţionale. În urma evaluării acestor adnotări primite am obţinut că în ambele modele nu se respectă proprietatea de corectitudine. Astfel automatele finite au acelaşi comportament ca şi reţelele flux de lucru.


Bibliografie

1. 
   Păstrăvanu, O. Aplicaţii ale reţelelor Petri în studierea sistemelor cu evenimente discrete. Ed. Gh. Asachi, Iaşi, 2002, 238p.
   
2. 
   J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation. Addison Wesley, 2001.
   
3. 
   P. Massuthe, W. Reisig, and K. Schmidt, “An Operating Guideline Approach to the SOA,” Annals of Mathematics, Computing & Teleinformatics, vol. 1, no. 3, pp. 35–43, 2005.