Metody formalne

Witam serdecznie na kolejnym wykładzie z „Inżynierii oprogramowania”!


Tematem dzisiejszego wykładu są metody formalne, czyli metody oparte na matematyce. Metody matematyczne (np. widoczne na slajdzie funkcje trygonometryczne) są szeroko wykorzystywane w wielu obszarach nauk technicznych, więc nic dziwnego, że próbuje się je stosować również w inżynierii oprogramowania.



Plan wykładów



Wykład ten można traktować jako rozwinięcie poprzedniego wykładu dotyczącego języka UML. Zarówno język UML, jak i metody formalne służą do opisu systemów informatycznych i różnych ich aspektów.


Ponadto wykład ten jest również – w jakimś sensie – kontynuacją wykładu nt. kontroli jakości oprogramowania.


Cztery filary zapewnienia jakości


Tam mówiliśmy głównie o testowaniu i przeglądach. Metody formalne są trzecią drogą, chociaż trzeba przyznać, że w praktyce droga ta jest rzadko uczęszczana.


Jakość oprogramowania


Na wykładzie dotyczącym kontroli jakości była przytoczona definicja jakości wg Crosby’ego, zgodnie z którą jakość jest rozumiana, jako zgodność z wymaganiami. Można powiedzieć, że idea metod formalnych opiera się właśnie na tej definicji jakości z tym, że zakłada się, iż wymagania zostały sformułowane na gruncie matematycznym (czyli bardzo precyzyjnie) i można metodami matematycznymi zbadać, czy dany program jest zgodny z tą specyfikacją. Często przedmiotem takiego badania są wybrane właściwości programu lub systemu informatycznego.


Słabości testowania 

Istotność metod formalnych wynika z obserwacji Dijkstry, który – jak pewnie Państwo pamiętacie – powiedział, że testowaniem nie można wykazać, że błędów nie ma. Jedynie korzystając z metod matematycznych można pokazać, że program ma określone właściwości i jest zgodny ze specyfikacją.


Dowodzenie poprawności 


Jedną z osób, której informatyka zawdzięcza bardzo wiele jest brytyjski profesor Tony Hoare. Urodził się w 1934 roku.


Najpierw interesował się filologią klasyczną, potem językiem rosyjskim.


W 1959 roku zainteresował się statystyką matematyczną i programowaniem komputerów. Zainteresowania te rozwijał w Moskwie, gdzie badał głównie problemy automatycznej translacji.


Po powrocie do Wielkiej Brytanii w 1960 roku wymyślił algorytm sortowania znany jako Quicksort i opracował w firmie Elliott Brothers jeden z pierwszych kompilatorów języka Algol 60, który właśnie został opracowany i którego rozwinięciem był później język Pascal.


W 1968 roku został profesorem w Belfaście w Irlandii Północnej, a w 1977 roku przeszedł na Uniwersytet w Oxfordzie.


W 1980 roku został uhonorowany nagrodą Turinga, która jest w informatyce odpowiednikiem nagrody Nobla.




Przytoczyłem biografię prof. Hoara, gdyż wniósł on bardzo wiele do rozwoju metod formalnych. Znana jest tzw. hipoteza Hoare’a, zgodnie z którą dowodzenie programów rozwiązuje problemy poprawności, dokumentacji i kompatybilności. Hipoteza ta stanowi dla wielu osób punkt wyjścia i uzasadnienie prowadzenia badań w zakresie metod formalnych



Profesor Hoare zaproponował także podejście do specyfikowania i dowodzenia poprawności programów zwane często logiką Hoare’a. Właściwości programu (lub fragmentu programu) Q opisuje się za pomocą pary predykatów P i R. Predykat P opisuje tzw. warunek wstępny, natomiast R jest warunkiem końcowym. Wyrażenie, które widzimy na slajdzie można przeczytać w następujący sposób: jeżeli jest spełniony warunek P, to po wykonaniu instrukcji Q spełniony będzie warunek R.


Oto bardzo prosty przykład. Jeżeli zmienna X ma wartość n, to po wykonaniu instrukcji przypisania zmiennej Y wyniku funkcji silnia od X, zmienna Y będzie miała wartość n!.


To podejście zostało wykorzystane w praktyce przy definicji języka ANNA służącego do specyfikowania programów zapisanych w języku Ada.



Podejścia do specyfikacji formalnej


Generalnie formalne metody specyfikowania programów można podzielić na oparte na modelach i aksjomatyczne. Metody oparte na modelach każą opisać zachowanie się programu za pomocą zestawu standardowych pojęć takich jak zbiór, sekwencja. Natomiast metody aksjomatyczne specyfikują program przez podanie zestawu zdań, które mają być spełnione przez każdą poprawną implementację programu. Przypomina to aksjomaty Euklidesa dotyczące geometrii, stąd nazwa „metody aksjomatyczne”.


Plan wykładu

Plan wykładu jest następujący. Najpierw omówimy specyfikacje aksjomatyczne.

Potem przedstawię związane z nimi tzw. implementacje niestandardowe. Jest to dość ciekawe zjawisko o charakterze anomalii, z którego trzeba sobie zdawać sprawę.


Ostatnią część wykładu chciałbym poświęcić sieciom Petriego, bardzo ciekawej metodzie specyfikowania programów i systemów współbieżnych.


Zaczynamy od specyfikacji aksjomatycznych.



Specyfikacje aksjomatyczne


Załóżmy, że chcemy opracować elektroniczną książkę telefoniczną. Książka, jak to w przykładach akademickich bywa, będzie bardzo prosta: z każdym nazwiskiem będzie związany numer telefonu.


Przechodząc do oprogramowania będziemy potrzebowali trzy typy danych:





Nasza książka będzie oferować cztery operacje i każda z nich będzie funkcją. Najważniejszą operacją jest operacja Lookup (po angielsku „poszukaj”) odszukująca w książce telefonicznej numer telefonu podanego abonenta.


Operacja ta ma dwa parametry wejściowe: nazwisko abonenta N i książkę telefoniczną D, w której należy poszukać numer telefonu.


Wynikiem jest numer telefonu podanego abonenta.




Aby móc dodawać nowych abonentów do książki telefonicznej wprowadzimy operację Add (po angielsku „dodaj”).


Operacja ta ma trzy parametry wejściowe: nazwisko abonenta N, numer telefonu F i książkę telefoniczną D, do której chcemy dodać informacje o tym abonencie.


Jako wynik dostajemy nową książkę telefoniczną z dopisaną informacją o nowym abonencie.




Skoro możemy dodawać nowych abonentów, to powinniśmy także móc usuwać abonentów. W tym celu wprowadzimy operację Delete (po angielsku „usuń”).


Parametrami wejściowymi dla tej operacji są:



W rezultacie dostajemy książkę telefoniczną, z której informacja o danym abonencie została usunięta.




Ostatnią operacją jest operacja Empty. Jest to operacja bezargumentowa. Jej wynikiem jest pusta książka telefoniczna, do której można coś zapisać za pomocą operacji Add.

Zauważmy, że taką książkę telefoniczną, jak ją widzimy na slajdzie można otrzymać na bardzo wiele sposobów.


Na przykład można do pustej książki telefonicznej dodać informację o Kowalskim, a potem o Malinowskim.


W zapisie funkcyjnym można to przedstawić jako złożenie trzech operacji pokazanych na slajdzie.


Można też do pustej książki najpierw dodać informację o Malinowskim, a potem o Kowalskim.


W zapisie funkcyjnym wyglądałoby to tak, jak na slajdzie w prawym dolnym rogu.




Spróbujmy teraz formalnie opisać te operacje. Wykorzystamy notację RAISE. Naszą książkę telefoniczną nazwiemy Directory.



Typy danych wykorzystywanych przez nasze oprogramowanie są w tej notacji deklarowane jako „class type” (typy klas).



Dla każdej funkcji określana jest tzw. sygnatura, będąca odpowiednikiem nagłówka funkcji. Po nazwie funkcji i dwukropku podawany jest typ wartości funkcji. Przykład funkcji bezargumentowej jest podany na slajdzie.



Jeśli funkcja ma parametry wejściowe, to w sygnaturze opisuje się je na zasadzie iloczynu kartezjańskiego. Podaje się nazwy typów kolejnych parametrów oddzielając je między sobą symbolem „x ”. Sposób opisu 3-parametrowej funkcji Add jest przedstawiony na slajdzie.




Sygnatury pozostałych funkcji są zbudowane na podobnej zasadzie.




Przejdźmy teraz do sformułowania aksjomatów opisujących działanie tych funkcji. Jeżeli szukamy numeru telefonu abonenta Abo w pewnej książce telefonicznej


która powstała z książki d przez dodanie do niej informacji, że Abo ma numer telefonu t,


to oczywiście szukany numer telefonu jest równy t.


Formalnie można to zapisać jak na slajdzie.




Jeżeli szukamy numeru telefonu Abo w książce, która powstała z książki d przez dodanie informacji o innym abonencie niż Abo,


to musimy szukać dalej, czyli szukać informacji o abonencie Abo w „starej” książce d.


Formalnie, w notacji RAISE, można to zapisać za pomocą frazy ELSE pokazanej na slajdzie.




Kolejny aksjomat można sformułować następująco: usunięcie czegokolwiek z pustej książki telefonicznej daje pustą książkę telefoniczną.


Formalnie można to zapisać jak na slajdzie




Kolejny aksjomat, dotyczący usuwania, można by sformułować następująco: jeżeli jakaś książka powstała z książki d przez dodanie do niej informacji o numerze telefonu t abonenta Abo,


to usunięcie abonenta Abo z tej książki daje starą książkę d.


Za pomocą notacji RAISE można to zapisać w sposób pokazany na slajdzie.




Jeżeli dana książka telefoniczna powstała z książki d przez dodanie informacji o innym abonencie niż Abo, a my chcemy usunąć z książki Abo, to tego innego należy w książce pozostawić, a usunąć Abo ze starej książki d. Innymi słowy, należy ze starej książki d usnąć abonenta Abo i dodać do wyniku informację o tym innym abonencie.


Korzystając z notacji RAISE można to zapisać w sposób pokazany na slajdzie.




Zastanówmy się, czy ta definicja jest poprawna. Czy faktycznie określa takie zachowanie systemu, jakiego oczekujemy?




Załóżmy, że nasza książka telefoniczna ma dwa zapisy dotyczące abonenta Kowalskiego.




Zgodnie z podaną definicją otrzymamy książkę „krótszą” o jednego Kowalskiego, ale drugi zapis dotyczący Kowalskiego pozostanie. Możemy zaakceptować takie działanie naszego sytemu, albo też możemy odpowiednio zmienić specyfikację. Ten drugi wariant pozostawiam do rozwiązania w charakterze ćwiczenia.

Plan wykładu



Ze specyfikacjami aksjomatycznymi wiąże się zjawisko o charakterze anomalii zwane implementacjami niestandardowymi. Postaram się to wyjaśnić na bardzo prostym przykładzie.



Implementacje niestandardowe




Załóżmy, że chcemy napisać specyfikację prostego pakietu wykonującego elementarne operacje arytmetyczne na liczbach naturalnych. Punktem wyjścia będzie dla nas aksjomatyczna definicja operacji arytmetycznych, którą można znaleźć w wielu książkach. Zawiera ona dwa aksjomaty. Po pierwsze, dodanie zera do dowolnej liczby x daje liczbę x.


W drugim aksjomacie występuje pojęcie następnika. Następnik jest to kolejna liczba naturalna względem podanej, np. następnikiem 2 jest 3, a następnikiem 3 jest 4. Niech funkcja succ(y) (od angielskiego „successor”, czyli następnik) podaje następnik liczby y.




Zgodnie z drugim aksjomatem dodanie do liczby x następnika liczby y daje następnik sumy liczb x i y.


Na przykład 2 + 4 można traktować jako sumę 2 i następnika 3. Zgodnie z tym aksjomatem 2 + 4 jest równe następnikowi 2 + 3. Jak wiemy, 2 + 3 = 5 i następnikiem 5 jest 6. Zatem faktycznie zgadza się: 2 + 4 jest równe 6.




Załóżmy, że stałą 0 będziemy realizować jako bezargumentową funkcję zero.


Funkcja succ będzie miała jeden argument będący liczbą naturalną i jej wynikiem też będzie liczba naturalna.


Operacja dodawania będzie realizowana jako funkcja plus, która będzie miała dwa argumenty będące liczbami naturalnymi i wynikiem będzie też liczba naturalna (dla uproszczenia posłużyłem się tutaj typem int, który obejmuje również liczby ujemne, ale z punktu widzenia problemu, o którym chcę powiedzieć nie ma to znaczenia).




Uwzględniając przyjęty interfejs dla naszego mikro-modułu, przepisujemy oba nasze aksjomaty zastępując operator dodawania funkcją plus a stałą 0 funkcją zero.




Nasze oczekiwania są oczywiście takie, że funkcja plus zwróci dla argumentów 2 i 3 wartość 5. Ale czy na pewno zawsze tak będzie?




Załóżmy, że ktoś postanowił zrealizować nasz mikro-moduł w sposób niestandardowy. Funkcja zero zwraca zawsze wartość 1.


Funkcja następnika, succ, zwraca liczbę dwa razy większą od podanej.


Natomiast funkcja plus zwraca iloczyn podanych liczb.




Ponieważ x razy 1 jest zawsze równe x, zatem pierwszy aksjomat przy tym rozwiązaniu zawsze będzie spełniony.


Prawdą jest także, że x razy 2y jest zawsze równe 2 razy xy. Czyli nasz mikro-pakiet spełnia także drugi aksjomat.



Problem polega na tym, że wywołanie funkcji plus z naszego pakietu dla parametrów 2 i 3 zwróci liczbę 6, a my spodziewamy się liczby 5. W czym tkwi problem? Proszę się nad tym zastanowić.


Plan wykładu



Specyfikacje aksjomatyczne i związane z nimi implementacje niestandardowe dotyczyły programów sekwencyjnych. Ale wiele systemów informatycznych ma charakter współbieżny. Do ich modelowania wykorzystuje się sieci Petriego, jedną z najbardziej popularnych koncepcji dotyczących matematycznych podstaw informatyki.


Carl Adam Petri



Autor tego pomysłu, Carl Adam Petri, urodził się w 1926 roku w Lipsku.


W wieku 36 lat obronił rozprawę 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, nazwana sieciami Petri’ego, bardzo szybko uzyskała wręcz niesamowitą popularność i była stosowana nie tylko do opisu procesów obliczeniowych, ale także systemów transportowych, produkcyjnych i innych.


Od 1988 roku Carl Petri jest honorowym profesorem Uniwersytetu w Hamburgu.



Co to za gra?


Być może inspiracją dla profesora Petri’ego były gry planszowe. Wiele z nich jest, w istocie, opartych na procesach współbieżnych. Na slajdzie mamy planszę do jednej z bardzo popularnych gier.


W grze tej może brać udział do czterech graczy. Każdy z nich ma po cztery pionki: jeden czerwone, drugi zielone itd.


Każdy pionek ma z góry wyznaczoną drogę do przebycia.


Jeden ruch odpowiada przesunięciu się na tej drodze o tyle pozycji, ile oczek pokazuje rzucona kostka. W przypadku zilustrowanym na slajdzie rzucona kostka pokazała dwa oczka.


Teraz do gry włączył się pionek zielony.


On ma swoją drogę do przebycia po tej planszy.


Jeśli rzucona kostka będzie miała 6 oczek,


to na planszy pojawi się następująca konfiguracja. Mamy zatem na jednej planszy jakby dwa procesy: czerwony, który jest o dwa miejsca bliżej celu, i zielony, który jest o sześć miejsc bliżej swojego celu. Pewnie Państwo już rozpoznaliście tę grę. Tak, to gra zwana chińczykiem.



Terminologia


Oto najmniejsza sieć Petri’ego. Jak się za chwilę przekonamy, jest ona pod kilkoma względami bardzo podobna do planszy gry w chińczyka.

Po pierwsze, w sieci Petri’ego mamy miejsca oznaczane kółkami.




W chińczyku też były miejsca z tym, że miały one kształt kwadracików.



W sieci Petriego mamy znaczniki, które mogą przechodzić z miejsca do miejsca.

Są one odpowiednikami pionków w chińczyku.




Znacznik przemieszczając się z jednego miejsca w drugie przechodzi przez tzw. przejście (niektórzy nazywają to tranzycją od ang. transition).


W chińczyku odpowiednikiem przejścia jest granica między dwoma miejscami. Nie ma ona w tej grze żadnego znaczenia, więc jest niezauważalna. W sieciach Petriego z przejściami mogą być związane różnego rodzaju akcje. Gdy znacznik przechodzi przez przejście, z którym związano akcję, to ta akcja jest wtedy wykonywana.




Ponadto mamy łuki wejściowe i wyjściowe. Łuki wejściowe zawsze prowadzą od miejsca do przejścia, a łuki wyjściowe od przejścia do miejsca. Jak widać, punktem odniesienia jest tutaj przejście. Łuki wejściowe „wchodzą” do przejścia, a łuki wyjściowe „wychodzą” z przejścia.



W sieciach Petri’ego przemieszczenie znacznika z jednego miejsca do drugiego odbywa się zawsze poprzez przejście. Lewa sieć na slajdzie jest źle zbudowana, bo brakuje na niej przejścia.



Przejścia nie mogą następować bezpośrednio po sobie. Zawsze po przemieszczeniu znacznika przez przejście musi on trafić do jakiegoś miejsca. Lewa sieć na slajdzie jest źle zbudowana, bo mamy dwa, bezpośrednio po sobie następujące, przejścia.


Bardzo prosty przykład



Rozważmy w charakterze przykładu proces opisujący zachowanie się czytelnika w bibliotece. Upraszczając możemy przyjąć, że czytelnik znajduje się w dwóch stanach: albo czeka na książkę, albo ją czyta. Możemy to zamodelować za pomocą następującej sieci Petriego.


Każdemu stanowi odpowiada jedno miejsce: z czekaniem związane jest miejsce waiting (czyli po angielsku „oczekujący”), natomiast z czytaniem - reading (po angielsku „czytający”). Czytanie jest poprzedzone wykonaniem akcji start_reading (zacznij czytanie), a kończy się wykonaniem akcji stop_reading (zakończ czytanie). Znacznik znajduje się w miejscu waiting , czyli nasz czytelnik teraz czeka.




Ponieważ czeka, zatem gotowe jest do odpalenia przejście start_reading – zaznaczono je na slajdzie kolorem czerwonym. Przejście stop_reading nie jest czerwone, bo nie jest ono gotowe do odpalenia, gdyż nie ma znacznika w bezpośrednio poprzedzającym je miejscu reading .




Po pewnym czasie dochodzi do odpalenia przejścia start_reading i znacznik przechodzi do miejsca reading.



Teraz przejście stop_reading jest gotowe do odpalenia, a przejście start_reading nie.



Po odpaleniu przejścia stop_reading znacznik przechodzi do miejsca waiting i przejście start_reading staje się gotowe do odpalenia. Zatem wróciliśmy do konfiguracji sieci, która była na samym początku.




Załóżmy teraz, że mamy dwóch czytelników w bibliotece i każdy z nich albo czeka, albo czyta. Jak można to zamodelować za pomocą sieci Petri’ego?



Okazuje się, że bardzo prosto. Wystarczy wprowadzić do poprzedniej sieci drugi znacznik reprezentujący drugiego czytelnika. Oczywiście możliwych konfiguracji sieci jest teraz więcej niż poprzednio.



Na przykład jeden znacznik może wciąż czekać, a drugi może przejść do miejsca reading



i wrócić do waiting .


Możliwy jest też inny wariant.




Jeden znacznik przejdzie z waiting do reading .



A drugi zaraz podąży za nim.




Potem znów jeden przechodzi przez stop_reading do waiting .




I po pewnym czasie drugi podąży za nim. Ta wielość możliwych zachowań (czyli indeterminizm) jest cechą charakterystyczną systemów współbieżnych i sieci Petri’ego, które takie systemy modelują.



Przejście konfliktowe


W procesach współbieżnych czasami zależy nam na wzajemnym wykluczaniu się procesów: z dwóch (lub więcej) procesów tylko jeden może wejść do rejonu krytycznego. Taką sytuację można zamodelować w sieciach Petri’ego za pomocą tzw. punktu decyzyjnego.



Mamy lewy proces związany z przejściem (tranzycją) t1 i obejmujący miejsca p10, p11.



Jest też prawy proces związany z tranzycją t2 i obejmujący miejsca p20, p21.



Miejsce p0 jest tzw. punktem decyzyjnym.




W konfiguracji pokazanej na slajdzie przejścia t1 i t2 są gotowe do odpalenia, bo w każdym miejscu, z którego wychodzi łuk wejściowy znajdują się znaczniki (chodzi o miejsca p10, p0 i p20).



Jeśli odpalone zostanie przejście t1, to zostaną „skonsumowane” znaczniki znajdujące się w miejscach p10 i p0, natomiast pojawi się znacznik w miejscu p11 „wyprodukowany” przez łuk wyjściowy tranzycji t1. W rezultacie żadne przejście nie będzie gotowe od odpalenia. Lewe (t1) nie, bo nie ma znaczników w miejscach p10 i p0. Prawe przejście (t2) też nie jest gotowe do odpalenia, bo co prawda jest znacznik w p20 ale brakuje znacznika w p0 (jeśli tranzycja ma dwa łuki wejściowe, to znaczniki muszą być w obu miejscach związanych z tymi łukami, aby tranzycja była gotowa do odpalenia).



Wróćmy na chwilę do konfiguracji początkowej. Oczywiście, jest możliwe zachowanie alternatywne. Zamiast przejścia t1 może być odpalone przejście t2.



Otrzymamy wówczas konfigurację prezentowaną na slajdzie, która jest konfiguracją symetryczną do poprzedniej. Jak więc widać, metodą punktu decyzyjnego możemy modelować wzajemne wykluczanie się procesów.


Inny przykład


Spróbujmy teraz naszkicować, tytułem przykładu, model systemu pracującego w układzie klient-serwer.


Klient pracuje w pętli nieskończonej. Wykonuje operację t1, potem jakieś nieistotne operacje pomocnicze, operację t2, znów nieistotne operacje pomocnicze i na końcu operację t3.


Serwer jest wywoływany przez klienta między operacjami t1 a t2. Po wywołaniu serwera klient niezależnie dalej prowadzi swoje obliczenia łącznie z operacją t2.


Obsługa wywołania jest realizowana przez serwer za pomocą pętli typu while. Aby sprawdzić, czy kontynuować obliczenia serwer wywołuje funkcję t4 (może to być np. sprawdzenie stanu bazy danych). Jeśli obliczenia mają być kontynuowane, to najpierw są wykonywane jakieś mało istotne operacje pomocnicze, potem operacja t5 i znów nieistotne operacje pomocnicze.


Po wyjściu z pętli while serwer kończy swoje obliczenia i przekazuje sterowanie do klienta, który nie wykona operacji t3 dopóki nie otrzyma wyników pracy serwera




Zamodelowanie pracy serwera jest proste. Mamy do wykonania w pętli dwie operacje, zatem tworzymy sieć składającą się z dwóch przejść t1 i t2, dodajemy dwa miejsca i łączymy wszystko łukami tak, aby znacznik mógł krążyć po sieci w sposób zgodny z programem serwera.




Zamodelowanie pracy klienta odbywa się na podobnej zasadzie. Mamy trzy sekwencyjne operacje wykonywane w pętli. Zatem tworzymy „ścieżkę” tranzycji t1, t2 i t3, po czym dodajemy łuk zwrotny do miejsca związanego z łukiem wejściowym tranzycji t1.



Jak teraz połączyć te dwa modele częściowe, aby dostać model całości? Jak się okazuje, nie jest to trudne.


Wystarczy dodać dwa łuki: łuk wyjściowy z tranzycji t1 i łuk wejściowy do tranzycji t3.




Na początku tranzycja t1 jest gotowa do odpalenia, czyli klient jest gotowy do wykonania operacji t1.




Po jej wykonaniu dochodzi do zrównoleglenia pracy klienta i serwera: każdy z łuków wyjściowych tranzycji t1 „generuje” swój znacznik. Klient jest gotowy do wykonania operacji t2, natomiast serwer może już wykonać t4. Załóżmy, że obie operacje zostają wykonane równolegle.



Wówczas znaczniki przemieszczają się i gotowe są do odpalenia tranzycje t5 oraz t3. Zauważmy, że lewe dolne miejsce pełni rolę punktu decyzyjnego: albo zostanie odpalona tranzycja t5 albo t3. Załóżmy, że serwer musi wykonać operację t5.




Zatem znacznik przechodzi przez tranzycję t5 i tranzycja t3 przestaje być gotowa do odpalenia. Ale jest teraz gotowe do odpalenia przejście t4. Jest to jedyne gotowe do odpalenia przejście, więc nie trudno zgadnąć, co się teraz stanie.



Przejście t4 zostaje odpalone i znów są gotowe do odpalenia przejścia t5 i t3. Załóżmy, że tym razem serwer zakończył swoje obliczenia.



Zatem odpalona zostaje tranzycja t3, zostają „skonsumowane” oba znaczniki związane z łukami wejściowymi i pojawia się znacznik w miejscu na samej górze, czyli wróciliśmy do konfiguracji początkowej. Jak więc widać, sieci Petri’ego mogą służyć do modelowania istniejącego oprogramowania. Jeśli dobrze zbudujemy model oprogramowania i pokażemy (np. udowodnimy), że model ten ma pewną interesującą nas właściwość, to możemy ufać, że oprogramowanie również posiada tę właściwość zwłaszcza, jeśli potwierdzają to testy i wyniki inspekcji.


Skróty notacyjne


W sieci Petri’ego z ostatniego przykładu występował fragment z przejściem t3 przedstawiony na slajdzie.


Aby przejście t3 było gotowe do odpalenia znaczniki muszą być we wszystkich miejscach związanych z łukami wejściowymi.




Rozważmy sieć Petri’ego z dwoma łukami wejściowymi wychodzącymi z tego samego miejsca. Ile (przynajmniej) znaczników musi być w górnym miejscu, aby tranzycja t30 była gotowa do odpalenia?


Tak jest – potrzeba przynajmniej dwóch znaczników, bo każdy łuk wejściowy „konsumuje” jeden znacznik.




Zamiast rysować dwa łuki wejściowe wychodzące z tego samego miejsca można narysować jeden łuk wejściowy i dopisać przy nim liczbę dwa – tak jak na slajdzie.


Wówczas, aby tranzycja t300 była gotowa do odpalenia, w górnym miejscu muszą być przynajmniej dwa znaczniki.




Odpalenie tranzycji t300 spowoduje zabranie dwóch znaczników z miejsca górnego i wstawienie jednego znacznika do miejsca dolnego.



Jeśli chcielibyśmy, by przejście t300 generowało np. trzy znaczniki, to powinniśmy przy łuku wyjściowym dopisać trójkę tak, jak to zrobiono na slajdzie.



Wówczas odpalenie tranzycji t300 spowoduje pojawienie się w dolnym miejscu trzech znaczników.


Problem zastoju


Spróbujemy teraz wykorzystać sieci Petri’ego do analizy systemu informatycznego pod kątem zastoju. Załóżmy, że w pewnym biurze są dwa komputery, A i B, które współdzielą drukarkę LP i dysk HD.


Najistotniejszy, z punktu widzenia naszej analizy, fragment oprogramowania komputera A można sprowadzić do sekwencji pięciu instrukcji.


Najpierw komputer A wykonuje operację AllocateLP, za pomocą której przydzielona zostaje mu drukarka LP (jeśli drukarka będzie zajęta, to wykonanie operacji AllocateLP będzie się przedłużało).


Potem komputer A wykonuje operację AllocateHD, w efekcie której zostaje mu przydzielony dysk HD.


Mając przydzieloną drukarkę LP i dysk HD, komputer A przysyła dane z dysku na drukarkę – jest to reprezentowane za pomocą operacji UseHDandLP.


Po wykorzystaniu tych urządzeń komputer A najpierw zwalnia dysk HD,


a następnie drukarkę LP.


Program komputera B jest podobny. Najpierw jest sekwencja operacji przydzielających dysk HD i drukarkę LP.


Potem następuje wykorzystanie obu tych urządzeń.


A na końcu urządzenia zostają zwolnione.


Jak nie trudno zauważyć, przedstawione rozwiązanie ma pewną wadę.




Załóżmy, że komputer A wykonał pierwszą operację, dzięki czemu ma przydzieloną drukarkę LP, a komputer B wykonał w tym czasie swoją pierwszą operację i ma przydzielony dysk HD.



Jeśli teraz komputer A przejdzie do wykonywania operacji przydziału dysku, AllocateHD, to jego działanie zostanie wstrzymane, bowiem dysk HD jest już przydzielony do komputera B.



Komputer B, przechodząc do wykonania operacji przydziału drukarki, AllocateLP, też zostanie zawieszony, gdyż drukarka jest już przydzielona komputerowi A i nie została jeszcze przez ten komputer zwolniona operacją ReleaseLP, gdyż komputer A jest zawieszony w oczekiwaniu na zwolnienie dysku przez komputer B. Mamy zatem zastój. Żaden z procesów nie może dalej kontynuować swoich obliczeń. Jest to ewidentna wada tak zaprogramowanego systemu. Jak tę wadę można by wykryć na poziomie sieci Petri’ego?



Program komputera A można łatwo zamodelować za pomocą sekwencji tranzycji tak, jak to pokazano na slajdzie. W sieci Petri’ego dodano jeszcze łuk zwrotny, by pokazać, że ta sekwencja operacji może być powtarzana wielokrotnie.



Program komputera B można zamodelować na tej samej zasadzie.



Dysk HD jest zasobem, który jest konieczny do wykonania operacji AllocateHD i jest zwalniany za pomocą operacji ReleaseHD. Zamodelujemy go wprowadzając związane z nim miejsce HD. Operacje AllocateHD będą miały dodatkowe łuki wejściowe prowadzące z miejsca HD, natomiast operacje ReleaseHD będą miały dodatkowe łuki wyjściowe idące do miejsca HD.



Drukarkę LP zamodelujemy na tej samej zasadzie.



Początkową konfigurację sieci Petri’ego przedstawiono na slajdzie. Znaczniki są w czterech górnych miejscach, w związku z czym przejścia AllocateHD i AllocateLP są gotowe do odpalenia.



Załóżmy, że zostanie odpalona tranzycja AllocateHD. Wówczas będziemy mieli konfigurację przedstawioną na slajdzie: będą gotowe do odpalenia obie tranzycje AllocateLP.



Jeśli zostanie odpalona prawa, to przejdziemy do konfiguracji pokazanej na kolejnym slajdzie. Cechą charakterystyczną tej konfiguracji jest brak przejścia gotowego do odpalenia. W ten właśnie sposób ujawnia się w sieci Petri’ego zastój.


Plan wykładu


Czas na podsumowanie wykładu.


Specyfikacje aksjomatyczne


Mówiliśmy o specyfikacjach aksjomatycznych. Do ilustracji wybraliśmy notację RAISE i zapisaliśmy w niej specyfikację aksjomatyczną elektronicznej książki telefonicznej. Jedną z operacji wykonywanych przez tę książkę jest operacja lookup służąca do znajdowania numeru telefonu podanego abonenta w podanej książce telefonicznej. Jak widać na slajdzie, specyfikacje aksjomatyczne mają często charakter rekurencyjny – operacja lookup jest zdefiniowana za pomocą operacji lookup.


Implementacje niestandardowe



Mówiliśmy też o implementacjach niestandardowych. Są to takie implementacje, które spełniają warunki stawiane przez specyfikację aksjomatyczną ale dają wyniki sprzeczne z naszymi oczekiwaniami. Problem polega na złym użyciu takiej implementacji. Zamiast pisać 2 powinniśmy napisać succ(succ(zero())). Podobnie powinniśmy przedstawić trójkę i szóstkę – wówczas nie byłoby problemu. Oczywiście, byłoby to mało wygodne. Aby uniknąć tego typu sytuacji najlepiej wzbogacić specyfikację formalną o kilka nawet prostych testów akceptacyjnych takich, jak ten pokazany na dole slajdu jako „Nasze oczekiwania”.


Sieci Petri'ego 


Wiele uwagi poświęciliśmy sieciom Petri’ego. Między innymi pokazaliśmy jak za ich pomocą modelować oprogramowanie.


Problem zastoju


Przedstawiłem też, na przykładzie, modelowanie i analizę związane z wykrywaniem zastoju.