[ Pobierz całość w formacie PDF ]
ÿþ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
start czytania
czytanie
start czekania
Znakowanie sieci
czekanie
start czytania
czytanie
start czekania
Znakowanie sieci
czekanie
start czytania
czytanie
start czekania
Znakowanie sieci
czekanie
start czytania
czytanie
start czekania
Znakowanie sieci dwaj czytelnicy
czekanie
start czytania
czytanie
start czekania
Wielość możliwych zachowań (indeterminizm)
Znakowanie sieci
- definicja formalna
Uporządkowaną czwórkę N=(P,T,A,Mo) nazywamy siecią znakowaną
jeżeli:
N=(P,T,A) jest sieciÄ…
Mo: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ść.
[ Pobierz całość w formacie PDF ]
