Inżynieria

Oprogramowania

Sieci Petriego

Adam Carl Petri

Urodził się w 1926 r. w Lipsku.

W wieku 36 lat obronił pracę doktorską pt. „Komunikacja z

automatami”, w której przedstawił pomysł opisu procesów
współbieżnych za pomocą notacji graficznej opartej na
solidnych podstawach matematycznych.

Koncepcja ta, zwana siecią Petri’ego, zyskała dużą

popularność nie tylko w odniesieniu do procesów
obliczeniowych ale także systemów transportowych,
produkcyjnych i innych.

Najmniejsza sieć Petriego

Definicja formalna

Uporządkowaną trójkę postaci N=(P,T,A)

nazywamy siecią, jeżeli spełnione są warunki:

P jest niepustym zbiorem miejsc

T jest niepustym zbiorem przejść (tranzycji)
takim, że P ∩ T=Ø

A jako podzbiór (P × T) U (T × P) jest zbiorem
łuków sieci

Sieć jako graf

Sieci Petriego przedstawiane są jako skierowane

grafy dwudzielne G=(V,A), dla których węzłami
są elementy zbiorów P i T tzn. V=P U T a łukami
- pary relacji A.

Wszystkie pojęcia zdefiniowane dla grafów

skierowanych (np. droga, cykl, graf spójny)
obowiązują również w odniesieniu do sieci.

Niepoprawne sieci Petriego

Przykład – czytelnik w bibliotece

czekanie

czytanie

start czytania

start czekania

Znakowanie sieci

czekanie

czytanie

start czytania

start czekania

Znakowanie sieci

czekanie

czytanie

start czytania

start czekania

Znakowanie sieci

czekanie

czytanie

start czytania

start czekania

Znakowanie sieci – dwaj czytelnicy

czekanie

czytanie

start czytania

start czekania

Wielość możliwych zachowań (indeterminizm)

Znakowanie sieci
- definicja formalna

Uporządkowaną czwórkę N=(P,T,A,M

o

) nazywamy siecią znakowaną

jeżeli:

N=(P,T,A) jest siecią

M

o

:P→Z jest funkcją która każdemu miejscu sieci przyporządkowuje

liczbę całkowitą nieujemną, interpretowaną jako liczba znaczników
umieszczonych wstępnie w danym miejscu.

Znakowaniem sieci nazywamy dowolną funkcję M:P→Z, i znakowanie

ulega zmianie w wyniku wykonywania przejść.

Przejście można wykonać jeżeli jest ono aktywne tzn. każde jego

miejsce wejściowe zawiera co najmniej jeden znacznik.

Wykonanie przejścia powoduje usunięcie znacznika z każdego z jego

miejsc wejściowych i dodanie nowego znacznika do każdego z jego
miejsc wyjściowych

Charakterystyczne konstrukcje sieciowe
- program sekwencyjny

Charakterystyczne konstrukcje sieciowe
- program współbieżny

Charakterystyczne konstrukcje sieciowe
- wzajemne wykluczanie

Charakterystyczne konstrukcje sieciowe
- komunikacja synchroniczna procesów

Charakterystyczne konstrukcje sieciowe
- komunikacja asynchroniczna procesów

Model sygnalizacji świetlnej

Model protokołu komunikacyjnego

Podsumowanie

„Testowaniem nie można wykazać braku błędów,

można jedynie wykazać ich obecność” (Dijkstra)

Jedynie korzystając z metod formalnych można

pokazać, że oprogramowanie ma określoną
własność.

Jeżeli dobrze zbudujemy model oprogramowania

w postaci sieci Petriego i udowodnimy, że model
ten posiada określoną własność, to możemy
ufać, że oprogramowanie również posiada tę
własność.