Pentru verificarea caracteristicilor de performanţă ale sistemelor distribuite s-au încercat diverse procedee de formalizare, inclusiv şi cel al reţelelor Petri[1], care dispun de un şir de atuuri cum ar fi: simplitatea, generalitatea şi adaptabilitatea. Iar extensiile acestora permit investigaţii ale unei clase şi mai largi de sisteme distribuite reale complexe. Trecerea de la reţele Petri clasice la cele colorate poate fi comparată cu trecerea de la limbajele de programare de nivel jos la limbajele de programare de nivel înalt. Respectiv, datorită reţelelor colorate[2], s-a simplificat cu mult verificarea proprietăţilor comportamentale ale sistemelor reale complexe. Pentru a demonstra cum reţelele Petri colorate[3, 4] surprind în mod corespunzător gradul dorit de acurateţe al modelării, vom considera un sistem care constă dintr-un protocol de comunicaţii în care o persoană trimite (sender) un anumit număr de pachete, iar alta le primeşte (receiver). În acest sistem se poate întâmpla ca unele pachete să se piardă sau să le depăşească pe altele. Din acest motiv este necesar ca unele pachete să fie retransmise şi să se ignore dublurile sau pachetele care nu respectă ordinea indicată. De asemenea, ne intereasează în mod deosebit să putem obţine informaţia referitoare la pachetele care se pierd şi cele care ajung cu succes, sau informaţia referitoare la faptul de câte ori a fost trimis un pachet până a ajunge cu succes la destinaţie. Aparent acest protocol este simplu, dar şi destul de complex pentru a efectua o investigaţie mai profundă. Pentru a putea efectua o analiză calitativă şi cantitativă a acestui sistem sa utilizat simulatorul CPN Tools[5], care dispune de un şir de instrumente destinate acestui fapt. Evidenţiem trei componente principale ale sistemului: componenta expeditorului, reţeaua şi componenta destinatarului. Fiecare din aceste componente este modelată cu ajutorul formalismului reţelelor Petri colorate prin utilizarea culorilor care specifică: numărul pachetului ce urmează a fi transmis, conţinutul de tip textual al mesajelor şi produsul cartezian al acestor culori. Iar pentru a obţine informaţia referitoare la pachetele pierdute şi la cele ajunse cu succes la destinaţie se va utiliza câte o locaţie suplimentară pentru fiecare caz. Locaţia LostPack va furniza informaţia despre pachetele pierdute, iar locaţia LostAck ne va indica numărul de pachete ajunse cu succes la destinaţie. Pentru a vedea de câte ori a fost transmis un pachet de asemenea se va utiliza o locaţie suplimentară, care nu influenţează comportamentul sistemului. Locaţia SentPack va calcula frecvenţa de transmitere a fiecărui pachet. În urma modelării acestui sistem şi simulării acestuia cu ajutorul instrumentului CPN Tools am obţinut următoarea informaţie: a fost pierdut pachetul cu numărul doi; cu succes au fost transmise trei pachete; pachetul cu numărul unu a fost transmis de patru ori, cu numărul doi de şase ori, cu numărul trei de două ori.