Next: Omówienie uzyskanych wyników Up: autoref_pol Previous: autoref_pol
Tematyka badañ
Praca po¶wiêcona jest zagadnieniom zwi±zanym z pojêciem równowa¿no¶ci obserwacyjnej (behawioralnej), odgrywaj±cym fundamentaln± rolê w wiêkszo¶ci zaproponowanych metod systematycznego konstruowania oprogramowania. Zgodnie z szeroko przyjêt± metodologi±, konstruowanie systemu rozpoczyna siê od ¶cis³ej specyfikacji jego wymaganych w³asno¶ci i dopuszczalnych zachowañ. Semantyka formalizmu budowania specyfikacji okre¶la klasê modeli specyfikacji, reprezentuj±cych dopuszczalne realizacje specyfikowanego systemu. Proces konstruowania oprogramowania sk³ada siê z ci±gu kroków, prowadz±cych od specyfikacji wymagañ do koñcowej realizacji, a ka¿dy z nich opisuje implementacjê systemu lub jego sk³adowej.
Zasada ukrywania nieistotnej informacji prowadzi do pojêcia implementacji behawioralnej, polegaj±cej na dopuszczeniu tych realizacji systemu, które oberwacyjnie spe³niaj± dan± specyfikacjê. Jako przyk³ad rozwa¿my pojêcie modu³u, posiadaj±cego operacje eksportowane, czyli widoczne dla otoczenia, oraz pewne operacje ukryte, lokalne, czyli niedostêpne z zewn±trz. W podej¶ciu behawioralnym za poprawn± implementacjê uwa¿amy ka¿dy modu³, którego obserwowalne zachowanie (tzn. wyniki operacji eksportowanych) spe³nia wymagania specyfikacyjne. Innym podej¶ciem do implementacji behawioralnej jest dupuszczenie, wraz z danym modelem, wszystkich modeli obserwacyjnie równowa¿nych, tzn. nieodró¿nialnych za pomoc± dostêpnych operacji (obserwacji). Przyk³adowo, dwa modu³y s± obserwacyjnie równowa¿ne, gdy po wykonaniu dowolnego ci±gu operacji eksportowanych, w ka¿dym z nich otrzymamy takie same wyniki.
Równowa¿no¶æ behawioralna wprowadzona zosta³a niezale¿nie w wielu odmianach dla ró¿nych modeli systemów. Szczególnie intensywnie pojêcie to jest studiowane w kontek¶cie specyfikacji algebraicznych i w teorii procesów wspó³bie¿nych.
W dziedzinie specyfikacji algebraicznych modelami specyfikacji - a wiêc te¿ matematycznymi obiektami reprezentuj±cymi specyfikowane systemy - s± algebry wielorodzajowe nad ustalon±, zadan± w specyfikacji sygnatur±. Równowa¿no¶æ obserwacyjna ([9]) studiowana by³a tutaj w wielu wersjach, w zale¿no¶ci m. in. od wybranego jêzyka specyfikacji, zbioru obserwowalnych operacji, czy te¿ od wyboru klasy modeli (por. [1]). Najczê¶ciej przyjmowane jest podej¶cie, w którym w sygnaturze wyró¿niamy podzbiór rodzajów obserwowalnych, co pozwala na okre¶lenie nierozró¿nialno¶ci w algebrze za pomoc± obserwowalnych kontekstów. W uproszczeniu, dwie algebry s± równowa¿ne je¶li ich algebry ilorazowe przez relacje nierozró¿nialno¶ci s± izomorficzne (mówimy, ¿e równowa¿no¶æ obserwacyjna jest faktoryzowana przez relacje nierozró¿nialno¶ci).
Dla procesów wspó³bie¿nych istnieje wiele ró¿nych pojêæ równowa¿no¶ci behawioralnej, spo¶ród których najczê¶ciej stosowane w praktyce s± ró¿ne odmiany równowa¿no¶ci bisymulacyjnej (ang. bisimilarity, por. [8]). Podstawowa idea jest tu nastêpuj±ca: dwa procesy uwa¿amy za równowa¿ne, gdy potrafi± one nawzajem symulowaæ swoje zachowanie, tzn. gdy istnieje tzw. relacja bisymulacji pomiêdzy nimi.
Od dawna dostrzegano koncepcyjne podobieñstwo pomiêdzy algebraicznymi równowa¿no¶ciami obserwacyjnymi a równowa¿no¶ciami opartymi na bisymulacji, natomiast nie istnia³o jednolite podej¶cie, pozwalaj±ce uj±æ te istotnie ró¿ne definicyjnie pojêcia we wspólnym modelu. W niniejszej rozprawie podjêto próbê rozwi±zania tego problemu.
Next: Omówienie uzyskanych wyników Up: autoref_pol Previous: autoref_pol Slawomir Lasota 2000-03-17