Index of /rozprawy2/10134

Pełen tekst

(1)Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie Wydział Elektrotechniki, Automatyki, Informatyki i Elektroniki. ROZPRAWA DOKTORSKA MGR IN Z˙ .. P IOTR M ATYASIK. M ODELOWANIE I ANALIZA SYSTEMÓW WBUDOWANYCH Z ZASTOSOWANIEM ALGEBRY PROCESÓW. XCCS. P ROMOTOR : dr hab. Marcin Szpyrka. Kraków, 18.05.2009.

(2) 2.

(3) Składam serdeczne podzi˛ekowania Panu dr hab. Marcinowi Szpyrce za nieoceniona˛ pomoc, której udzielił mi w trakcie pisania tej pracy..

(4) 2.

(5) Spis tre´sci. 1. Wprowadzenie 1.1. Przedstawienie problemu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2. Cel badań i teza pracy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3. Zawarto´sc´ pracy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 9 10 12 13. 2. Algebry Procesów 2.1. Historia algebr procesów . . . . . . . . . . . 2.2. Calculus of Communicating Systems . . . . . 2.3. Communicating Sequential Processes . . . . 2.4. Algebra of Communicating Processes . . . . 2.5. Language of Temporal Ordering Specification 2.6. Narz˛edzia . . . . . . . . . . . . . . . . . . . 2.6.1. CADP . . . . . . . . . . . . . . . . . 2.7. Edinburgh Concurrency Workbench . . . . . 2.7.1. CWB-NC . . . . . . . . . . . . . . . 2.7.2. MOTOR . . . . . . . . . . . . . . . . 2.8. Zastosowania . . . . . . . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. 15 16 16 17 17 18 18 18 19 19 20 20. 3. Algebra CCS 3.1. Rachunek elementarny . . . . . 3.2. Rozszerzenie czasowe TCCS . . 3.3. Rachunek z przesyłaniem danych 3.4. Równowaz˙ no´sc´ modeli CCS . . 3.5. Logika Hennessy-Milnera . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. 21 21 27 31 34 39. 4. Algebra XCCS 4.1. Warstwa graficzna . . . . . . . . . . . . . . . 4.2. Warstwa algebraiczna . . . . . . . . . . . . . 4.3. Reguły konstruowania modelu . . . . . . . . 4.4. Konwersja diagramów XCCS do algebry CCS 4.4.1. Eliminacja elementów junction . . . . 4.4.2. Numerowanie agentów . . . . . . . . 4.4.3. Wyliczanie priorytetów agentów . . . 4.4.4. Reetykietowanie połaczonych ˛ portów ˙ 4.4.5. Eliminacja niepozadanych ˛ połacze´ ˛ n . 4.4.6. Eliminacja operatora przeplatania . . 4.4.7. Generacja skryptu CCS . . . . . . . . 4.5. Przykłady . . . . . . . . . . . . . . . . . . . 4.5.1. Model pi˛eciu filozofów . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. . . . . . . . . . . . . .. 45 45 47 48 48 49 51 52 53 53 55 55 56 56. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. 5.

(6) 4.5.2. Model sygnalizacji s´wietlnej . . . . . . . . . . . . . . . . . . . . . . . 4.5.3. Czuwak aktywny . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 58 60. 5. Algebra XCSS z przesyłaniem danych 5.1. Warstwa graficzna . . . . . . . . . . . . . . . . . 5.2. Warstwa algebraiczna . . . . . . . . . . . . . . . 5.2.1. Deklaracje . . . . . . . . . . . . . . . . . 5.2.2. Definicje agentów . . . . . . . . . . . . . 5.3. Modelowanie z wykorzystaniem VP-XCCS . . . 5.4. Konwersja diagramów XCCS do algebry VP-CCS 5.5. Przykłady . . . . . . . . . . . . . . . . . . . . . 5.5.1. Producent - konsument . . . . . . . . . . 5.5.2. Czytelnicy i pisarze . . . . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. 63 63 64 64 66 67 69 69 69 72. 6. Inez XCCS Editor 6.1. Architektura programowa edytora . . 6.2. Uz˙ ytkowanie edytora . . . . . . . . . 6.2.1. Tworzenie diagramów . . . . 6.2.2. Tworzenie agentów i portów . 6.2.3. Podstawowe operacje edycyjne 6.2.4. Tworzenie połacze´ ˛ n . . . . . . 6.2.5. Skalowanie diagramu i siatka . 6.2.6. Okno ustawień . . . . . . . . 6.2.7. Eksport diagramów . . . . . . 6.2.8. Menu aplikacji . . . . . . . . 6.3. Format danych . . . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. 75 75 75 75 76 76 78 78 81 81 81 83. 7. Modelowanie systemów wbudowanych z wykorzystaniem VP-XCCS na przykładzie robota Hexor 7.1. Robot Hexor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.2. Koncepcja systemu sterujacego ˛ . . . . . . . . . . . . . . . . . . . . . . . . . . 7.3. Model systemu sterujacego ˛ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.4. Test modelu robota . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.5. Implementacja systemu sterujacego ˛ . . . . . . . . . . . . . . . . . . . . . . . .. 87 87 88 90 94 95. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. . . . . . . . . . . .. 8. Podsumowanie 103 8.1. Wnioski końcowe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 8.2. Perspektywy dalszych badań . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 A. Gramatyka wyra˙zen´ dla rachunku elementarnego XCCS. 107. B. Gramatyka wyra˙zen´ dla rachunku XCCS z przesyłaniem danych. 109. Literatura. 113.

(7) Spis rysunków. 3.1 3.2 3.3 3.4 3.5 3.6 3.7. Grafy pochodnych agentów A i B . . . . . . . . . . . . . . . . Graf pochodnych agenta C . . . . . . . . . . . . . . . . . . . Graficzna reprezentacja procesu w CCS . . . . . . . . . . . . Graficzna reprezentacja procesu C . . . . . . . . . . . . . . . Graf pochodnych agenta C . . . . . . . . . . . . . . . . . . . Grafy pochodnych dla silnie równowaz˙ nych agentów . . . . . Grafy pochodnych dla słabo równowaz˙ nych i obserwacyjnie agentów . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.8 Grafy pochodnych dla słabo równowaz˙ nych agentów . . . . . 3.9 Grafy pochodnych dla agentów A i B . . . . . . . . . . . . . 3.10 Model skrzyz˙ owania . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . kongruentnych . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 36 37 37 38. 4.1 4.2 4.3 4.4 4.5 4.6 4.7 4.8 4.9 4.10 4.11 4.12 4.13 4.14 4.15 4.16 4.17. Graficzna reprezentacja agenta XCCS . . . . . . . . . . . . Graficzna reprezentacja połaczenia ˛ portów w XCCS . . . . . Agenci XCCS bez połaczenia ˛ . . . . . . . . . . . . . . . . . Połaczenie ˛ jeden do wielu i wiele do jednego w XCCS . . . Warunek asymetrycznej trójprzechodnio´sci . . . . . . . . . Połaczenie ˛ jeden do wielu . . . . . . . . . . . . . . . . . . . Połaczenie ˛ jeden do wielu - rozwini˛ecie . . . . . . . . . . . Połaczenie ˛ wiele do jednego . . . . . . . . . . . . . . . . . Połaczenie ˛ wiele do jednego - rozwini˛ecie . . . . . . . . . . Przykładowy model XCCS - diagram . . . . . . . . . . . . . Przykładowy model XCCS po operacji indeksowania portów Przykład z rys. 4.11 po operacji reetykietowania portów . . . Przykład z rys. 4.11 po eliminacji niechcianych połacze´ ˛ n . . Model pi˛eciu filozofów w XCCS . . . . . . . . . . . . . . . Schemat skrzyz˙ owania . . . . . . . . . . . . . . . . . . . . Model skrzyz˙ owania – diagram XCCS . . . . . . . . . . . . Model systemu automatycznego zatrzymywania pociagu ˛ . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . .. 45 46 46 46 48 49 49 50 50 50 52 54 55 56 58 58 60. 5.1 5.2 5.3. Graficzna reprezentacja agenta VP-XCCS . . . . . . . . . . . . . . . . . . . . Model producent - konsument . . . . . . . . . . . . . . . . . . . . . . . . . . Model czytelników i pisarzy – warstwa graficzna . . . . . . . . . . . . . . . .. 63 70 72. 6.1 6.2 6.3 6.4. Inez XCCS editor . . . . . . . . . . . . . . . . Inez – menu kontekstowe agenta . . . . . . . . Inez – edycja definicji algebraicznej agenta . . Inez – selekcja elementów, widok na zakładk˛e agentów . . . . . . . . . . . . . . . . . . . . . Inez – tworzenie połacze´ ˛ n. . . . . . . . . . . .. 76 77 77. 6.5. . . . z . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . definicjami algebraicznymi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 24 26 26 27 30 35. 78 79 7.

(8) 6.6 6.7 6.8 6.9. Inez – wybór portów wewn˛etrznych Inez – dodawanie elementu Junction Inez – dodawanie elementu Junction Inez – okno ustawień . . . . . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. . . . .. 79 80 80 81. 7.1 7.2 7.3 7.4 7.5 7.6 7.7 7.8 7.9. Robot Hexor . . . . . . . . . . . . . . . . . . Model warstwowy sterowania robotem Hexor Model zadań warstwy HexorNG . . . . . . . Kolejka FIFO . . . . . . . . . . . . . . . . . Agent Ir . . . . . . . . . . . . . . . . . . . . Agent Tentacles . . . . . . . . . . . . . . . . Agent Sonar . . . . . . . . . . . . . . . . . . Agent Move . . . . . . . . . . . . . . . . . . Agent Hexor . . . . . . . . . . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. . . . . . . . . .. 88 89 89 91 91 91 92 92 93. 4.1. Priorytety agentów z rys. 4.11 . . . . . . . . . . . . . . . . . . . . . . . . . .. 53. 5.1. Typy podstawowe VP-XCCS . . . . . . . . . . . . . . . . . . . . . . . . . . .. 64. Spis tabel.

(9) 1. Wprowadzenie. Poczatki ˛ stosowania metod formalnych w inz˙ ynierii oprogramowania si˛egaja˛ połowy poprzedniego wieku ([8]). Juz˙ u zarania informatyki jako nauki pojawiła si˛e potrzeba modelowania oraz weryfikacji produktów informatycznych. Złoz˙ ono´sc´ nawet pierwszych systemów informatycznych oraz trudno´sci w ich analizie zwróciły uwag˛e naukowców na formalizacj˛e oraz komputerowo wspomagane metody posiadajace ˛ matematyczne podstawy oraz sći´sle okre´slona˛ składni˛e i semantyk˛e. Szczególne znaczenie metodom formalnym zacz˛eto przypisywać w końcu lat 70. Na okres ten datuje si˛e zauwaz˙ alny szybki wzrost kosztów wytwarzania oprogramowania, przy jednoczesnym obniz˙ aniu kosztów sprz˛etu komputerowego. Koszty te były szczególnie odczuwalne ze wzgl˛edu na towarzyszacy ˛ im wzrost zawodno´sci wytwarzanego oprogramowania. Juz˙ wtedy zauwaz˙ ono, z˙ e w cyklu z˙ ycia oprogramowania najbardziej kosztowne sa˛ bł˛edy powstajace ˛ ˙ w poczatkowej ˛ fazie jego projektowania. Wydawało si˛e wówczas, ze szybki rozwój podej´sc´ formalnych moz˙ e stanowić rozwiazanie ˛ pogł˛ebiajacego ˛ si˛e kryzysu. Niestety zbyt wygórowane oczekiwania wzgl˛edem metod formalnych spowodowały, z˙ e nie mogły one spełnić pokładanych w nich nadziei. W efekcie powstał mit, który okre´sla metody formalne jako narz˛edzie wyłacznie ˛ dla informatyków teoretyków, całkowicie nieprzydatne w praktycznych zastosowaniach. Poczawszy ˛ od lat 80. datuje si˛e wi˛ec trwajacy ˛ spór dwóch przeciwstawnych pogladów. ˛ Z jednej strony przeciwnicy metod formalnych uwaz˙ aja˛ je za narz˛edzie całkowicie nieprzydatne w inz˙ ynierii oprogramowania, z drugiej strony zwolennicy metod formlanych staraja˛ si˛e wskazać moz˙ liwe obszary ich zastosowań, który moga˛ przynie´sc´ istotne korzy´sci inz˙ ynierii oprogramowania ([18, 19, 36]). W tym drugim podej´sciu szczególnie istotny jest wła´sciwy dobór stosowanego formalizmu i wła´sciwa ocena moz˙ liwo´sci jakie on za soba˛ niesie. Nie bez znaczenia jest równiez˙ wsparcie wybranej metody formalnej przez odpowiedniej jako´sci oprogramowanie, które pozwala w znacznym stopniu zautomatyzować proces weryfikacji konstruowanych modeli. Idea wspierania procesu wytwarzania oprogramowania przez metody formalne staje si˛e w ostatnich latach ponownie coraz bardziej popularna. Mimo trwajacej ˛ od lat 80. dyskusji na temat uz˙ yteczno´sci metod formalnych w inz˙ ynierii oprogramowania, ciagle ˛ rozwijane sa˛ istniejace ˛ podej´scia, a takz˙ e proponuje si˛e nowe metody ([23, 26, 29, 70]). Współcze´snie wi˛ekszo´sc´ instytucji zwiazanych ˛ z wytwarzaniem oprogramowania jest s´wiadoma konieczno´sci stosowania oraz dalszego rozwoju metod formalnych. Bardzo waz˙ nym w obszarze bezpieczeństwa systemów informatycznych jest wprowadzony przez Komisj˛e Europejska˛ standard ITSEC (Information Technology Security Evaluation Criteria), który okre´slił konieczno´sc´ stosowania metod formalnych w procesie ewaluacji oprogramowania dla czterech (z siedmiu) poziomów bezpieczeństwa. Dodatkowo standard ISO od roku 1999 rekomenduje zastosowanie metod formalnych powyz˙ ej piatego ˛ poziomu bezpieczeństwa. Zastosowanie metod formalnych moz˙ e przede wszystkim zwi˛ekszyć niezawodno´sc´ wytwarzanego oprogramowania. Jest to szczególnie istotne dla systemów okre´slanych jako krytyczne ze wzgl˛edu na bezpieczeństwo, tj. systemów, których bł˛edy działania moga˛ spowodować istot9.

(10) ne straty ekonomiczne, uszkodzenia fizyczne czy tez˙ moga˛ mieć wpływ na zdrowie lub z˙ ycie ludzi oraz na s´rodowisko naturalne ([64, 67, 69]). Z drugiej strony wykrycie bł˛edów na wczesnym etapie wytwarzania systemu moz˙ e znaczaco ˛ zredukować koszt jego wytworzenia. Koszty eliminacji bł˛edów znaczaco ˛ wzrastaja,˛ jez˙ eli bł˛edy te sa˛ wykrywane w pó´zniejszych etapach wytwarzania oprogramowania. Koszty weryfikacji i walidacji systemów krytycznych ze wzgl˛edu na bezpieczeństwo moga˛ przekraczać nawet 50% kosztów ich wytworzenia ([67]).. 1.1. Przedstawienie problemu Jak zostało juz˙ wspomniane moz˙ emy współcze´snie obserwować ponowny wzrost zainteresowania metodami formalnymi, widoczny przede wszystkim w rozwoju istniejacych ˛ podej´sc´ oraz wspierajacych ˛ je narz˛edzi komputerowych. Przede wszystkim podejmowane sa˛ próby dostosowania istniejacych ˛ rozwiaza´ ˛ n do potrzeb inz˙ ynierów praktyków. Niniejsza praca doktorska wpisuje si˛e w nurt tych poszukiwań. W´sród najwaz˙ niejszych współcze´snie grup metod formalnych stosowanych do modelowania i weryfikacji systemów wbudowanych moz˙ na wyróz˙ nić: • algebry procesów ([14, 15, 20, 26, 35, 57, 58]), • automaty czasowe ([2, 3, 4, 11]), • logiki temporalne ([24, 40, 41, 42, 61]), • sieci Petriego ([38, 62, 71, 72]). Zastosowanie dowolnego formalizmu prowadzi do celu poprzez konstruowanie róz˙ norodnych modeli abstrakcyjnych, które w zalez˙ no´sci od potrzeb w róz˙ nym stopniu ukazuja˛ poszczególne aspekty tworzonego systemu takie jak jego struktura, dynamika czy tez˙ funkcjonalno´sc´ . Szczególnie istotne, a zarazem najtrudniejsze do analizy sa˛ własno´sci dynamiczne systemu. Trudno´sci te istotnie wzrastaja˛ w przypadku systemów wbudowanych, które charakteryzuja˛ si˛e współbiez˙ no´scia˛ działania. Badania podj˛ete w ramach niniejszej pracy dotycza˛ rozwoju jednego z najbardziej popularnych rachunków algebr procesów CCS (Calculus of Communicating Systems, [26, 56, 57]). Algebry procesów sa˛ stosowane do opisu i analizy dynamiki systemów w sposób algebraiczny ([15]). Termin process wskazuje wła´snie na fakt, z˙ e model dotyczy dynamiki konstruowanego systemu, podczas gdy termin algebra oznacza, z˙ e do konstruowania tego opisu stosowane jest zaksjomatyzowane podej´scie algebraiczne. Inne popularne rachunki algebraiczne to: CSP (Communicating Sequential Processes, [35]), ACP (Algebra of Communicating Processes, [14]), LOTOS ([20]), RSL (Raise Specification Language, [28]), czy tez˙ rachunek π (πcalculus, [58]). Obszerny przeglad ˛ róz˙ nych formalizmów algebraicznych moz˙ na znale´zc´ w pracy [15]. W modelowaniu systemów współbiez˙ nych w algebrach procesów szczególny nacisk stawiany jest na analiz˛e obserwowanego z zewnatrz ˛ zachowania si˛e systemu i na dowodzenie równowaz˙ no´sci dwóch róz˙ nych modeli tego samego systemu. Istotnym jest przy tym, by modele te miały podobne wzory zachowań zewn˛etrznych, natomiast cz˛esto ignorowane sa˛ operacje, które reprezentuja˛ wewn˛etrzne komunikowanie si˛e elementów składowych takiego systemu. Modelowanie z uz˙ yciem algebr procesów jest wi˛ec podej´sciem iteracyjnym, w którym konstruowane sa˛ cz˛esto kolejne co raz bardziej szczegółowe modele tego samego systemu, za´s dost˛epne formalne metody analizy modeli pozwalaja˛ wykazać równowaz˙ no´sc´ poszczególnych iteracji. Drugim stosowanym podej´sciem jest wyraz˙ enie specyfikacji wymagań z zastosowaniem logiki modalnej ([26, 61]) i sprawdzenie, czy konstruowane modele spełniaja˛ poszczególne 10.

(11) formuły logiczne. Jednym ze stosowanych rachunków jest logika Hennessy-Milnera ([31]). Podej´scie to jest preferowane w sytuacji, gdy w trakcie budowania systemu dodaje si˛e do niego dodatkowa˛ funkcjonalno´sc´ , co zazwyczaj wyklucza moz˙ liwo´sci weryfikacji opartej o równowaz˙ no´sc´ modeli. Z punktu widzenia algebry CCS system współbiez˙ ny traktowany jest jako układ niezalez˙ nych cz˛esći zwanych agentami, które sa˛ połaczone ˛ ze soba˛ poprzez wymian˛e komunikatów. Terminy współbiez˙no´sc´ i komunikacja stanowia˛ dwa główne poj˛ecia tego rachunku. Jako agent traktowana jest kaz˙ da z cz˛esći systemu majaca ˛ swoja˛ własna˛ toz˙ samo´sc´ trwajac ˛ a˛ w czasie. Bar˙ ˙ ˙ dzo waznym załozeniem w rachunku CCS jest nierozróznianie poj˛ecia agenta i stanu, w którym si˛e on znajduje. Termin agent zawsze oznacza agenta pozostajacego ˛ w pewnym stanie. W wyniku wykonywania akcji agent zmienia swój stan, czyli jest przekształcany w innego agenta. Kaz˙ dy agent ma okre´slony zestaw akcji, które moz˙ e wykonać. Akcje te podlegaja˛ dwom klasyfikacjom. Z jednej strony akcje dzielimy na wej´sciowe i wyj´sciowe, co odzwierciedla kierunek przekazywania informacji. Z drugiej strony wyróz˙ niane sa˛ akcje widoczne (obserwowalne) z zewnatrz ˛ (z otoczenia) systemu i akcje niewidoczne stosowane do komunikacji wewn˛etrznej. Akcje sa˛ równiez˙ traktowane jako porty komunikacyjne, dzi˛eki którym agent moz˙ e wymieniać informacje ze swoim otoczeniem. Złoz˙ one systemy współbiez˙ ne moga˛ być postrzegane jako układy agentów wzajemnie si˛e ze soba˛ komunikujacych. ˛ Jednym z celów rachunku CCS jest moz˙ liwo´sc´ wyraz˙ enia dynamiki złoz˙ onego systemu poprzez operacje poszczególnych agentów go tworzacych. ˛ Równoczesne wykonanie przez dwóch agentów akcji o uzupełniajacych ˛ si˛e etykietach (akcji wej´sciowej i wyj´sciowej o tych samych nazwach) traktowane jest jako komunikacja mi˛edzy tymi agentami i oznaczane jest etykieta˛ τ . Akcje takie uwaz˙ ane sa˛ za nieobserwowalne z zewnatrz. ˛ Model w j˛ezyku CCS przeznaczony do automatycznego przetwarzania jest zapisywany jako plik tekstowy zawierajacy ˛ ciag ˛ wyraz˙ eń definiujacych ˛ system jako układ komunikujacych ˛ si˛e ze soba˛ agentów. W odniesieniu do komunikacji obowiazuj ˛ a˛ tutaj dwie zasady: • Komunikacja mi˛edzy dwoma agentami jest moz˙ liwa, jez˙ eli maja˛ one porty o uzupełniajacych ˛ si˛e etykietach. • Komunikacja jest moz˙ liwa mi˛edzy dowolnymi agentami, które maja˛ porty o uzupełniaja˛ cych si˛e etykietach. Załoz˙ enia te skutkuja˛ licznymi problemami przy modelowaniu bardziej złoz˙ onych systemów, w szczególno´sci, gdy chcemy uz˙ yć kilku kopii tego samego agenta. Z jednej strony pojawia si˛e konieczno´sc´ reetykietowania portów, by umoz˙ liwić komunikacj˛e w przypadku braku uzupełniajacych ˛ si˛e etykiet. Z drugiej strony konieczno´sc´ reetykietowania pojawia si˛e równiez˙ w sytuacji, gdy chcemy wyeliminować niepoz˙ adan ˛ a˛ komunikacj˛e. agent Fork = ’up.down.Fork; agent Phil = lup.rup.’ldown.’rdown.Phil; Listing 1.1. Model pi˛eciu filozofów – agenty Fork i Phil. Rozwaz˙ my znany z literatury problem pi˛eciu filozofów. Definicje agentów Phil i Fork przedstawiono na Listingu. 1.1 (porty wyj´sciowe sa˛ wyróz˙ nione znakiem ’). Konstrukcja modelu całego systemu w formie złoz˙ enia (układu) pi˛eciu agentów Phil i pi˛eciu agentów Fork prowadzi do systemu, który zachowuje si˛e niezgodnie z oczekiwaniami. W modelu takim brak jest portów o uzupełniajacych ˛ si˛e etykietach, co oznacza brak komunikacji mi˛edzy agentami. Inne problemy wyst˛epuja˛ w przypadku, gdy definicje agentów maja˛ postać taka˛ jak przedstawiona na Listingu. 1.2. W modelu zawierajacym ˛ pi˛ec´ kopii kaz˙ dego z tych agentów pojawiaja˛ si˛e dwa istotne bł˛edy: 11.

(12) ˙ • Zaden z filozofów nie moz˙ e wzia´ ˛c prawego widelca, bo w systemie brak jest prawych widelców. • Kaz˙ dy z filozofów moz˙ e wzia´ ˛c dowolny z widelców (ale jako lewy widelec).. agent Fork = ’lup.ldown.Fork; agent Phil = lup.rup.’ldown.’rdown.Phil; Listing 1.2. Model pi˛eciu filozofów dla – agenty Fork i Phil (wersja 2). Rozwiazaniem ˛ jego problemu jest zdefiniowanie dla kaz˙ dego z dziesi˛eciu agentów indywidualnej funkcji przeetykietowujacej ˛ porty. Rozwiazanie ˛ takie przedstawiono w podrozdziale 3.1. Definicja wła´sciwych funkcji przeetykietowujacych ˛ nie jest jednak w ogólnym przypadku zadaniem łatwym. W modelu zawierajacym ˛ kilkadziesiat ˛ agentów moz˙ na przeoczyć niepoz˙ adane ˛ połaczeniu ˛ lub nie zdefiniować wszystkich wymaganych. Wydaje si˛e wi˛ec konieczne wprowadzenie mechanizmu eliminujacego ˛ moz˙ liwo´sc´ wystapienia ˛ tego typu bł˛edów modelowania. Drugim istotnym problemem zwiazanym ˛ z wykorzystaniem algebry CCS jest brak j˛ezyka do modelowania wizualnego. Wi˛ekszo´sc´ współcze´snie stosowanych narz˛edzi wspierajacych ˛ proces wytwarzania oprogramowania dostarcza mechanizmów do wizualnego modelowania róz˙ nych aspektów budowanego systemu. W przypadku algebr CCS dost˛epne sa˛ wprawdzie grafy przepływu ([26, 57]), ale stanowia˛ one wizualizacj˛e opisanego algebraicznie modelu, a nie j˛ezyk modelowania.. 1.2. Cel badan´ i teza pracy Jako podstawowy cel podj˛etych badań przyj˛eto opracowanie rozszerzenia algebry procesów CCS, do formalizmu wyposaz˙ onego w graficzny j˛ezyk modelowania, który z jednej strony ułatwiałby konstruowanie modelu, a z drugiej eliminowałby opisane w poprzednim podrozdziale problemy modelowania czysto algebraicznego. Nowy j˛ezyk modelowania okre´slony jako XCCS (eXtended CCS) miał być z załoz˙ enia j˛ezykiem algebraiczno-graficznym. W warstwie algebraicznej postanowiono pozostawić operatory powiazane ˛ z opisem dynamiki pojedynczych agentów, natomiast do warstwy graficznej postanowiono przenie´sc´ operatory uz˙ ywane przy definiowaniu połacze´ ˛ n mi˛edzy agentami. Jako punkt wyj´scia do opracowania reprezentacji graficznej postanowiono przyja´ ˛c opisane w literaturze grafy przepływów. Notacja ta miała być jednak modyfikowana tak, by moz˙ liwe było jednoznaczne reprezentowanie wszystkich operatorów, które miały być przeniesione do warstwy graficznej. J˛ezyk CCS wyst˛epuje w dwóch podstawowych wersjach: rachunek elementarny i rachunek z przesyłaniem danych (Value Passing CCS). W tym drugim przypadku istnieje moz˙ liwo´sc´ parametryzowania agentów i ich akcji. Innymi słowy w algebrze VP CCS nie tylko moz˙ emy zamodelować fakt komunikacji mi˛edzy dwoma agentami, ale równiez˙ warto´sc´ przesyłana˛ podczas tej komunikacji. Przyj˛eto załoz˙ enie, z˙ e rozwijany j˛ezyk modelowania XCCS ma wyst˛epować w obu tych wersjach – elementarnej i sparametryzowanej, przy zachowaniu (jez˙ eli b˛edzie taka moz˙ liwo´sc´ ) jednolitej notacji graficznej. Jako kolejny warunek odnoszacy ˛ si˛e do rozwijanego formalizmu przyj˛eto załoz˙ enie o moz˙ liwo´sci konwersji modeli zapisanych z uz˙ yciem XCCS do zapisu czysto algebraicznego w algebrze CCS (lub odpowiednio VP CCS). Oznaczało to konieczno´sc´ opracowania algorytmów 12.

(13) konwersji z modelu graficzno-algebraicznego do modelu algebraicznego. Podej´scie takie umoz˙ liwia skorzystanie z istniejacych ˛ narz˛edzi do analizy modeli zapisywanych w algebrze CCS. Przyj˛eto równiez˙ załoz˙ enie, z˙ e wraz z opracowaniem koncepcji XCCS podj˛ete zostana˛ prace zwiazane ˛ z zaprojektowaniem i implementacja˛ narz˛edzi komputerowych wspierajacych ˛ stosowanie rozwijanego formalizmu. Rozwijane oprogramowanie miało nie tylko zawierać edytor do konstruowania warstwy graficznej, ale równiez˙ implementacje zdefiniowanych algorytmów konwersji. Podej´scie takie miało na celu dostarczenie jednocze´snie opisu nowego j˛ezyka modelowania wraz z oprogramowaniem umoz˙ liwiajacym ˛ weryfikacj˛e jego przydatno´sci. ˙ Podsumowujac, ˛ przyj˛ete tezy pracy mozna sći´sle sformułować nast˛epujaco: ˛ Moz˙liwe jest opracowanie algebraiczno-graficznego j˛ezyka modelowania bazujacego ˛ na algebrach procesów CCS oraz VP CCS, który: • b˛edzie umoz˙liwiał wizualne modelowanie struktury połacze´ ˛ n mi˛edzy agentami tworzacy˛ mi konstruowany system; • b˛edzie eliminował moz˙liwo´sc´ wystapienia ˛ bł˛edów modelowania dotyczacych ˛ połacze´ ˛ n mi˛edzy agentami, które pojawiaja˛ si˛e w modelowaniu z uz˙yciem j˛ezyka czysto algebraicznego; • wsparty przez odpowiednie oprogramowanie b˛edzie umoz˙liwiał uzyskanie równowaz˙nego modelu w j˛ezyku CCS (lub odpowiednio VP CCS) w sposób automatyczny.. 1.3. Zawarto´sc´ pracy Niniejsza rozprawa została zredagowana tak, aby w miar˛e moz˙ liwo´sci w pełny sposób przedstawić opracowany j˛ezyk modelowania XCCS, wraz z oprogramowaniem Inez wspierajacym ˛ jego stosowanie. Poniewaz˙ weryfikacja modeli XCCS odbywa si˛e po ich translacji do algebry CCS, w rozprawie przedstawiono równiez˙ opis algebr CCS, VP CCS, definicje podstawowych relacji bisymulacji stosowanych do analizy równowaz˙ no´sci modeli oraz skrócony opis logiki HML. Jako przykład praktycznego zastosowania j˛ezyka XCCS zaprezentowano model modułu sterujacego ˛ dla robota mobilnego Hexor. Zawarto´sc´ poszczególnych rozdziałów i dodatków (z pomini˛eciem wst˛epu) kształtuje si˛e nast˛epujaco: ˛ • Rozdział 2 zawiera wprowadzenie do algebr procesów z uwzgl˛ednieniem rysu historycznego. Zostały w nim opisane w skrócie róz˙ ne algebry procesów słuz˙ ace ˛ do modelowania formalnego takie jak: CCS, CSP, ACP i LOTOS. W rozdziale tym zamieszczono równiez˙ przeglad ˛ narz˛edzi wykorzystujacych ˛ powyz˙ sze metodologie do dowodzenie poprawno´sci oprogramowania. Rozdział zamyka zestawienie pokazujace ˛ moz˙ liwo´sci wykorzystanie wyz˙ ej wspomnianych narz˛edzi i formalizmów w inz˙ ynierii oprogramowania. • Rozdział 3 prezentuje szczegółowo algebr˛e CCS jako wiodac ˛ a˛ i słuz˙ ac ˛ a˛ za podstaw˛e do budowy algebry XCCS. Zostały w nim opisane poszczególne elementy algebry CCS poczawszy ˛ od rachunku elementarnego, poprzez rachunek z przesyłaniem danych, rozszerzenie czasowe, a kończac ˛ na definicjach relacji bisymulacji i logice HML. W ostatnim podrozdziale przedstawiono oprogramowanie CWB, które w praktyce implementuje załoz˙ enia tej algebry. • Rozdział 4 jest pierwszym rozdziałem, w którym prezentowane sa˛ oryginalne idee zawarte w rozprawie. Zawiera on opis proponowanej algebry XCCS. Omówione w nim zostały obie warstwy algebry XCCS – graficzna i algebraiczna, a takz˙ e przedstawiono algorytm konwersji modeli XCCS do elementarnego rachunku CCS. Na zakończenie rozdziału przedstawione zostały przykłady modeli XCCS. 13.

(14) • Rozdział 5 prezentuje rozszerzenie algebry XCCS o elementy umoz˙ liwiajace ˛ przesyłanie danych. Omówiono w nim zarówno rozszerzenia w warstwie graficznej jak i algorytm konwersji do modelu w algebrze VP CCS. Na zakończenie rozdziału przedstawione zostały przykłady sparametryzowanych modeli XCCS. • Rozdział 6 zawiera opis edytora Inez, który wykorzystuje i implementuje prezentowane w rozdziałach 4 i 5 rozwiazania. ˛ Zawarta jest w nim instrukcja uz˙ ytkownika oraz opis szczegółów technicznych prezentowanego programu. • Rozdział 7 prezentuje praktyczne zastosowanie zbudowanego narz˛edzia do modelowania rzeczywistego systemu wbudowanego, którym jest moduł sterujacy ˛ robota mobilnego Hexor. W rozdziale tym zademonstrowany został cały proces tworzenia oprogramowania sterujacego ˛ dla modułu robota, poczawszy ˛ od modelu formalnego, przez weryfikacj˛e, usuwanie bł˛edów, az˙ do implementacji w docelowym j˛ezyku programowania. • Rozdział 8 zawiera podsumowanie pracy. Poza wnioskami końcowymi zawarto w nim równiez˙ perspektywy dalszych badań dotyczacych ˛ algebry XCCS. • Dodatek A zawiera gramatyk˛e wyraz˙ eń rachunku elementarnego XCCS. • Dodatek B zawiera gramatyk˛e wyraz˙ eń rachunku XCCS z przesyłaniem danych.. Niniejsza rozprawa została opracowana w ramach grantu Hekate, realizowanego w Katedrze Automatyki AGH w latach 2007-2009.. 14.

(15) 2. Algebry Procesów. Pierwszym formalizmem zwiazanym ˛ z teoria˛ współbiez˙ no´sci były sieci Petriego zaprezentowane w pracy doktorskiej Carla A. Petriego w 1962 roku ([63]). W roku 1970 ukształtowały si˛e juz˙ trzy główne podej´scia dotyczace ˛ formalnego wnioskowania o programach komputerowych ([8]): • operacyjny, • denotacyjny, • aksjomatyczny. W semantyce operacyjnej program komputerowy był modelowany jako maszyna abstrakcyjna ([50]), w podej´sciu denotacyjnym program modelowany był jako funkcja transformujaca ˛ wej´scie w wyj´scie ([66]), za´s semantyka aksjomatyczna kładła nacisk na metody dowodzenia poprawno´sci oprogramowania ([27, 32]). Wła´snie podej´scie aksjomatyczne stanowiło baz˛e dla algebr procesów jako narz˛edzia do analizy i weryfikacji systemów reaktywnych. Systemem moz˙ e być cokolwiek przedstawiajacego ˛ „zachowanie”, np.: program komputerowy, akcje robota, człowiek itd, przy czym zachowanie to cało´sc´ akcji, jakie system moz˙ e wykonać z uwzgl˛ednieniem kolejno´sci, zalez˙ no´sci czasowych i prawdopodobieństw wystapienia. ˛ Akcje zwykle sa˛ dyskretne i rozdzielone w czasie. Fundamentem algebr procesów była obserwacja poczyniona przez Robina Milnera a dotyczaca ˛ algebraicznej struktury procesów współbiez˙ nych ([1]). Przykładowo, majac ˛ dwa procesy P i Q moz˙ na zbudować nowy proces R. Zachowanie nowo powstałego procesu R b˛edzie zalez˙ eć od tego jak zachowuja˛ si˛e procesy P i Q oraz od sposobu ich złoz˙ enia. Algebra procesów jest studium zachowania systemu współbiez˙ nego lub rozproszonego w rozumieniu algebraicznym. Oferuje ona moz˙ liwo´sc´ przedstawienia złoz˙ enia równoległego, alternatywy i sekwencji. Dodatkowo wyz˙ ej wymienione instrumentarium pozwala wyciaga´ ˛ c wnioski na temat tak opisanego systemu. Najcz˛esćiej jest to sprawdzanie czy spełnia on zadane własno´sci. Podstawowymi operatorami w algebrze procesów sa: ˛ • + – alternatywa, • ; – sekwencja, • k – złoz˙ enie. Posiadaja˛ one nast˛epujace ˛ własno´sci, zwane takz˙ e prawami statycznymi: x+y =y+x x + (y + z) = (x + y) + z x+x=x 15.

(16) (x + y); z = x; z + y; z (x; y); z = x; (y; z) xky=ykx x k (y k z) = (x k y) k z. 2.1. Historia algebr procesów Historia algebr procesów si˛ega lat 70. poprzedniego stulecia Zacz˛eły wtedy powstawać pierwsze znaczace ˛ prace dotyczace ˛ matematycznego uj˛ecia procesów współbiez˙ nych ([10]). W tym czasie Hans Bekiˇc opracował koncepcj˛e składania prostych procesów w bardziej złoz˙ one. Uz˙ ył w tym celu globalnych zmiennych. W jego podej´sciu stan systemu ξ był reprezentowany przez warto´sciowanie zmiennych. W zalez˙ no´sci od stanu systemu program wykonujac ˛ akcj˛e A mógł przej´sc´ do stanu końcowego (null) lub wykonać elementarna˛ akcj˛e f i przej´sc´ w stan f ξ pozostawiajac ˛ akcj˛e resztowa˛ A0 . Bekiˇc wprowadził symbole: t i cases oznaczaja˛ ce kompozycj˛e alternatywna,˛ ; oznaczajacy ˛ sekwencj˛e oraz // oznaczajacy ˛ pseudo-równoległe złoz˙ enie. Sformułował on równiez˙ prawo dotyczace ˛ pseudo-równoległego złoz˙ enia: (A//B)ξ = (cases Aξ : null → Bξ (f, A0 ) → f, (A0 //B)) t (cases Bξ : null → Aξ (f, B 0 ) → g, (A//B 0 )). (2.1). Powyz˙ sza definicja była pierwowzorem tego co pó´zniej nazwano expansion law dla algebry procesów ([8]).. 2.2. Calculus of Communicating Systems Teoretyczne podstawy CCS powstawały w latach od 1973 do 1980 i były dziełem głównie Robina Millner’a. W pracach [53, 54] rozwaz˙ ał on problemy stwarzane przez niekończace ˛ si˛e programy i niedeterminizm. Uz˙ ywał operatora ∗ do okre´slenia sekwencji, ? dla alternatywy i k dla złoz˙ enia równoległego. Nast˛epnie w artykułach [52, 55] Milner wprowadził grafy przepływów, które były inspiracja˛ dla XCCS. Zmianie uległy równiez˙ niektóre operatory: | oznaczało złoz˙ enie równoległe, a k zostało operatorem złoz˙ enia równoległego ograniczonego. Pojawiły si˛e tez˙ operatory restrykcji i reetykietowania. Bardzo waz˙ ny element dla CCS jak i dla teorii procesów wprowadził David Park formułujac ˛ poj˛ecie bisymulacji ([60]). W 1980 roku Matthew Hennessy i Robin Milner sformułowali podstawy CCS ([30]). Zdefiniowano wówczas równowaz˙ no´sc´ obserwacyjna˛ i silna˛ równowaz˙ no´sc´ obserwacyjna.˛ W wyz˙ ej wspomnianej publikacji zaprezentowana została takz˙ e logika Hennessy-Milnera, która pozwala na logiczna˛ charakterystyk˛e równowaz˙ no´sci procesów ([8]). W tym samym roku Milner opublikował prac˛e [56], w której po raz pierwszy została przedstawiona kompletna algebra procesów. Zawierała ona zbiór równań oraz model semantyczny. Sam Milner podkre´slił w swojej publikacji obliczeniowy aspekt proponowanego rozwiazania ˛ piszac ˛ o rachunku procesów. 16.

(17) 2.3. Communicating Sequential Processes Autorem algebry CSP jest Tony Hoare. W 1978 roku opublikował on prac˛e [33], w której przedstawił nowy formalizm oparty na paradygmacie komunikacji polegajacej ˛ na przesyłaniu wiadomo´sci. CSP posiada synchroniczna˛ komunikacj˛e i chroniony j˛ezyk poleceń. Hoare nie podał modelu ani semantyki, ale publikacja ta zainspirowała Milnera do rozwiazania ˛ problemu przesyłania wiadomo´sci w CCS w taki sam sposób ([8]). Model dla CSP został zaprezentowany w pracy [34]. Był on oparty na s´ladzie, czyli na sekwencji akcji jakie proces moz˙ e wykonać. Okazało si˛e jednak, z˙ e model ten jest niedoskonały. Brakowało w nim zachowania własno´sci zakleszczenia. Dlatego tez˙ Stephen Brookes, Tony Hoare i A. William Roscoe wprowadzili model okre´slony w ich pracy jako failure pairs, przedstawiony w pracy [21]. J˛ezyk, w którym go zastosowano nazwano Theoretical CSP. Pó´zniej okazało si˛e, z˙ e przyj˛ety model jest najmniej ograniczajacym ˛ modelem zachowujacym ˛ własno´sc´ zakleszczenia. Do semantyki j˛ezyka CSP nalez˙ y: • prefiks (a → P ), • złoz˙ enie sekwencyjne (;), • wybór zewn˛etrzny ([]), • wybór wewn˛etrzny (|∼|), • złoz˙ enie równoległe (| A |), • przeplatanie (|||), • ukrycie zdarzeń (\), • rekursja, • zakleszczenie (ST OP ), • poprawne zakończenie (SKIP ). Do badania procesów zdefiniowanych za pomoca˛ CSP uz˙ ywa si˛e tzw. s´ladu procesu, czyli skończonego ciagu ˛ zdarzeń jakie proces generuje. Nieco szerzej temat podejmuje semantyka uszkodzeń, która ponadto zawiera zdarzenia, których proces moz˙ e nie wykonać poda˛z˙ ajac ˛ po okre´slonym s´ladzie. Ponad nimi stoi semantyka uszkodzeń i rozbiez˙no´sci, która dodatkowo zajmuje si˛e zdarzeniami, które proces moz˙ e wygenerować nieskończenie wiele razy, poczynajac ˛ od okre´slonego stanu.. 2.4. Algebra of Communicating Processes W 1980 roku Jan Bergstra i Jan Willem Klop rozpocz˛eli prace nad problemem postawionym przez Jacobus’a W. de Bakker’a dotyczacym ˛ rozwiazaniami ˛ niestrzez˙ onych równań rekurencyjnych ([8]). Rezultatem tych przemy´sleń była praca [12], w której po raz pierwszy w literaturze pojawił si˛e termin algebra procesów. Pojawiła si˛e tam takz˙ e definicja algebry procesów z alternatywa,˛ sekwencja˛ i złoz˙ eniem równoległym wraz z o´smioma aksjomatami, które wcze´sniej wymienione operatory musza˛ spełniać. W opracowaniu tym brakowało jednak wyst˛epujacej ˛ w nazwie komunikacji. Dopiero w pracy [13] teoria po uzupełnieniu o aspekt komunikacyjny stała si˛e kompletna i została okre´slona jako ACP. 17.

(18) 2.5. Language of Temporal Ordering Specification LOTOS jest j˛ezykiem specyfikacji opracowanym dla formalnego opisu architektury OSI1 , ale moz˙ e być równiez˙ uz˙ ywany do specyfikowania rozproszonych systemów współbiez˙ nych jako takich. Badany system w j˛ezyku LOTOS przedstawiany jest jako zbiór procesów wchodza˛ ´ cych w interakcje oraz wymieniajacych ˛ dane mi˛edzy soba˛ oraz ze srodowiskiem ([16, 20, 37]). W j˛ezyku LOTOS system okre´slany jest przez zdefiniowanie temporalnej relacji mi˛edzy interakcjami, które definiuja˛ zewn˛etrzne obserwowalne zachowanie systemu. Jednakz˙ e wbrew temu co sugeruje pojawiajacy ˛ si˛e termin „temporalny”, opis ten nie jest tworzony w oparciu o logik˛e temporalna,˛ ale o algebry procesów ([56]). Drugim elementem tworzacym ˛ j˛ezyk LOTOS jest opis struktur danych oraz warto´sci. Cz˛esć´ ta oparta jest na formalnej teorii abstrakcyjnych typów danych i wzorowana była na ACT ONE ([25]). LOTOS przedstawia rozproszony system współbiez˙ ny jako proces. Zwykle jest on złoz˙ ony z wielu procesów składowych. Kaz˙ dy proces składowy moz˙ e składać si˛e z innych podprocesów, stad ˛ specyfikacja moz˙ e być rozpatrywana jako hierarchia zdefiniowanych procesów. Proces w j˛ezyku LOTOS jest encja,˛ która moz˙ e wykonywać nieobserwowalne akcje oraz wchodzić w interakcje z innymi procesami tworzacymi ˛ s´rodowisko.. 2.6. Narz˛edzia Niniejszy rozdział zawiera krótka˛ charakterystyk˛e narz˛edzi słuz˙ acych ˛ do modelowania i weryfikacji systemów ze szczególnym uwzgl˛ednieniem tych, które wykorzystuja˛ algebry procesów. Poniz˙ sze zestawienie nie jest kompletne i zawiera tylko pozycje, które posiadaja˛ ukonstytuowana˛ pozycj˛e w´sród narz˛edzi wykorzystujacych ˛ metody formalne, bad´ ˛ z sa˛ w jakim´s aspekcie zwiazane ˛ z rozwiazaniami ˛ prezentowanymi w dalszej cz˛esći pracy.. 2.6.1. CADP CADP jest skrótem od Construction and Analysis of Distributed Processes ([74]). Wczesńiej pakiet ten znany był jako CAESAR/ALDEBARAN Development Package. Jest to popularny zestaw narz˛edzi słuz˙ acy ˛ projektowaniu protokołów komunikacyjnych i systemów rozproszonych. CADP jest rozwijany przez zespół VASY przy INRIA2 . Wartym podkre´slenia jest, z˙ e jest to projekt bardzo aktywnie rozwijany i stale wspierany przez twórców. Ponadto CADP jest wykorzystywany w wielu projektach, np. weryfikacja protokołu IEEE 1394 oraz komponentów bibliotecznych j˛ezyka Erlang. CADP jest pakietem oferujacym ˛ szeroka˛ gam˛e narz˛edzi, poczawszy ˛ od prostych symulacji krokowych a skończywszy na weryfikacji modelowej (model checking). Składa si˛e na niego: • zestaw kompilatorów dla kilku formalizmów (j˛ezyk LOTOS, automaty, sieci automatów itp.), • zestaw narz˛edzi do sprawdzania równowaz˙ no´sci modeli, • zestaw narz˛edzi do weryfikacji modelowej dla logiki temporalnej, rachunku µ i innych, • zestaw algorytmów weryfikujacych, ˛ • zestaw narz˛edzi wizualnych, testujacych ˛ wydajno´sc´ itd. 1 2. 18. Open Systems Interconnection l’Institut National de Recherche en Informatique et en Automatique.

(19) CADP posiada modularna˛ budow˛e i moz˙ e być łatwo rozszerzane o nowe formalizmy dzi˛eki wykorzystaniu eksportu do formatów wymiany lub interfejsów programistycznych.. 2.7. Edinburgh Concurrency Workbench CWB jest automatycznym narz˛edziem umoz˙ liwiajacym ˛ manipulacj˛e i analiz˛e systemów ˙ ˙ ˙ współbieznych. Umozliwia sprawdzanie równowazno´sci, relacji preorder, sprawdzanie modelu z uz˙ yciem TCCS i SCSS ([59]). Do ciekawszych funkcji tego programu, poza moz˙ liwo´scia˛ definiowania zachowania agentów, nalez˙ y: • znalezienie ilo´sci stanów dla agentów posiadajacych ˛ ich skończona˛ liczb˛e, • wygenerowanie grafu tranzycji dla danego agenta, • znalezienie stanów deadlock i live-lock oraz listy tranzycji do nich prowadzacych, ˛ • znalezienie obserwacji o danej długo´sci, • sprawdzenie czy agent jest stabilny, • sprawdzenie czy agenty spełniaja˛ wybrane warunki równowaz˙ no´sci, • przeprowadzenie interaktywnej symulacji. Program CWB dost˛epny jest w postaci binarnej dla róz˙ nych systemów operacyjnych (Linux, SunOS, Win32). Zainteresowani moga˛ dokonać kompilacji programu ze z´ ródeł, które równiez˙ sa˛ udost˛epnione. Zaleta˛ kompilacji ze z´ ródeł jest moz˙ liwo´sc´ wybrania tylko interesujacych ˛ uz˙ ytkownika modułów programu.. 2.7.1. CWB-NC Concurrency Workbench of the New Century (CWB-NC) ([75]) jest narz˛edziem wykorzystujacym ˛ róz˙ ne techniki do specyfikacji i weryfikacji systemów współbiez˙ nych skończeniestanowych. CWB-NC zawiera PAC (Process Algebra Compiler), który pozwala na rozszerzenie dost˛epnych notacji lub do rozbudowy funkcjonalno´sci juz˙ zaimplementowanych. Moz˙ na w łatwy sposób dodać relacje równowaz˙ no´sci lub preorder czy tez˙ zmienić j˛ezyk wykorzystywany do specyfikacji systemu. Od swojej pierwsze edycji w 1996 roku CWB-NC jest wykorzystywany głównie przez grupy zajmujace ˛ si˛e protokołami komunikacyjnymi oraz systemami steruja˛ cymi procesami. Weryfikacj˛e systemu moz˙ na przeprowadzić na kilka sposobów. Pierwszy oparty jest na analizie osiagalno´ ˛ sci stanów. Uz˙ ytkownik specyfikuje system wykorzystujac ˛ jeden z dost˛epnych j˛ezyków opisu oraz podaje formuły logiczne okre´slajace ˛ stany, których system nie moz˙ e przyja´ ˛c. System sprawdza przestrzeń stanów w poszukiwaniu tych zabronionych. Je´sli takie istnieja,˛ to uz˙ ytkownikowi przekazywana jest informacja o sekwencji akcji, która do nich prowadzi. Drugi sposób weryfikacji systemu wspierany przez CWB-NC polega na wyspecyfikowaniu zachowania systemu za pomoca˛ logiki temporalnej (rachunek µ) i badaniu czy podane zalez˙ nosći sa˛ spełnione. Trzeci sposób weryfikacji polega na wyspecyfikowaniu zarówno modelu systemu jak i wymagań za pomoca˛ wybranego j˛ezyka opisu i badaniu ich wzajemnej równowaz˙ no´sci. 19.

(20) CWB-NC pozwala na specyfikacj˛e modelu za pomoca˛ nast˛epujacych ˛ notacji: • podstawowy CCS, • CCS z priorytetami, • CCS z czasem, • CSP, • Basic LOTOS.. 2.7.2. MOTOR MOTOR ([39]) jest s´rodowiskiem wykorzystujacym ˛ j˛ezyk Modest do opisu i analizy systemów stochastycznych i czasowych. Pozwala on na modelowanie systemów z twardymi jak i mi˛ekkimi wymaganiami czasowymi oraz aspektów QoS3 . Modest jest j˛ezykiem modelowania opartym o algebry procesów jak CCS i CSP. Posiada on jednak rozszerzenia pozwalajace ˛ na operowanie prostymi strukturami danych i obsług˛e wyjatków. ˛ Modest pozwala na zapis szerokiej gamy modeli od etykietowanych systemów przej´sc´ przez automaty czasowe do stochastycznych procesów jak łańcuchy Markowa i markowskie procesy decyzyjne. Analiza modeli zbudowanych w s´rodowisku MOTOR jest oparta o narz˛edzia z pakietu CADP ([74]).. 2.8. Zastosowania Jednym z bardziej oczywistych zastosowań algebr procesów jest badanie protokołów komunikacyjnych. Wia˛z˙ e si˛e to z semantyka˛ tego formalizmu i powiazaniem ˛ akcji z komunikacja˛ mi˛edzy agentami ([7]). Innym przykładem zastosowań jest specyfikowanie i weryfikacja systemów komputerowo zintegrowanego wytwarzania (CIM – Computer Integrated Manufacturing). Algebry procesów moga˛ tez˙ być wykorzystane do weryfikacji algorytmów komputerowych. Zastosowania algebr procesów w inz˙ ynierii oprogramowania opieraja˛ si˛e na kilku cechach jakie daje ten formalizm. Pozwala on na badanie równowaz˙ no´sci modeli, a konkretnie równowaz˙ no´sci mi˛edzy bardziej abstrakcyjnym modelem b˛edacym ˛ specyfikacja˛ systemu a „realnym” modelem systemu utworzonym na podstawie kodu programu. Inna˛ metoda˛ zastosowania algebr procesów jest zbudowanie za ich pomoca˛ modelu systemu i badanie istnienia stanów niepoz˙ adanych, ˛ albo bardziej ogólnie badanie wybranych wła´sciwo´sci systemu wyspecyfikowanych np. za pomoca˛ jakiej´s odmiany logiki temporalnej. Jakkolwiek metody formalne sa˛ stosowane w róz˙ nych dziedzinach przemysłu i przez róz˙ ne znane firmy jak choćby AT&T, Intel, Lucent, Motorola, to do powszechnego ich stosowania w inz˙ ynierii oprogramowania jest jeszcze daleko. Aktualnie pojawiaja˛ si˛e pierwsze ułatwienia pozwalajace ˛ na stosowanie ich w praktyce inz˙ ynierskiej jak choćby te przedstawione w pracach [65, 74] i wiele innych. Rozwiazanie ˛ przedstawione w rozdziałach 4, 5 i 6 pozostaje w tym nurcie.. 3. 20. Quality of Service.

(21) 3. Algebra CCS W niniejszym rozdziale przedstawiono wprowadzenie do algebry procesów CCS. Podrozdział 3.1 zawiera podstawowa˛ wersj˛e tego rachunku, podrozdział 3.2 prezentuje rozszerzenie czasowe, za´s w podrozdziale 3.3 omówiono wersj˛e z przesyłaniem danych. Zagadnienia zwia˛ zane z poj˛eciem równowaz˙ no´sci modeli przedstawiono w podrozdziale 3.4, za´s podstawowe informacje o logice HML w podrozdziale 3.5. Algebry procesów sa˛ uz˙ ywane przede wszystkim do opisu dynamiki systemu poprzez przedstawienie jego zachowania w postaci odpowiednich wyraz˙ eń algebraicznych. Szczególny nacisk kładziony jest na komunikacj˛e mi˛edzy procesami. Konstrukcja modelu w algebrze CCS polega na okre´sleniu z jakich procesów (agentów) składa si˛e rozwaz˙ any system oraz opisaniu dynamiki tych agentów. Kaz˙ dy z procesów moz˙ e być traktowany jako czarna skrzynka, która posiada swój identyfikator (nazw˛e) oraz zdefiniowany interfejs, czyli zbiór portów słuz˙ acych ˛ do komunikacji. Komunikacja procesu moz˙ e mieć dwojaki charakter – komunikacji z otoczeniem lub wzajemnej interakcji mi˛edzy procesami. Model w j˛ezyku CCS jest w rzeczywisto´sci ciagiem ˛ równań, konstruowanych z uz˙ yciem operatorów wła´sciwych dla danej wersji rozwaz˙ anego rachunku. W praktyce jest to zwykły plik tekstowy (zob. podrozdz. 2.7). Załoz˙ eniem przyj˛etym w algebrze CCS jest brak rozróz˙ nienia mi˛edzy agentem a jego stanem. Agent jest wyraz˙ eniem algebraicznym, a wykonanie kolejnych akcji przekształca go w nast˛epne wyraz˙ enie algebraiczne, które równiez˙ spełnia definicj˛e procesu CCS. W praktyce, przy modelowaniu systemu w CCS, wygodnie jest posługiwać si˛e poj˛eciem agenta przede wszystkim w kontek´scie procesu znajdujacego ˛ si˛e w pewnym konkretnym stanie, na przykład przed wykonaniem pierwszej akcji. Pozwala to przyporzadkowa´ ˛ c takiemu agentowi znaczac ˛ a˛ nazw˛e odpowiadajac ˛ a˛ funkcji jaka˛ pełni w modelowanym systemie oraz w łatwy sposób opisywać jego dalsze zachowanie.. 3.1. Rachunek elementarny W rachunku elementarnym komunikacja mi˛edzy agentami nie wia˛z˙ e si˛e z przesyłaniem danych. Fakt przesyłania danych mi˛edzy agentami modelowany jest przez zastosowanie oddzielnego portu dla kaz˙ dej z przesyłanych warto´sci. W celu formalnego zdefiniowania składni i semantyki j˛ezyka elementarnego CCS przyjmuje si˛e nast˛epujace ˛ załoz˙ enia: • dany jest zbiór nazw A, a, b, c, . . . ∈ A; ¯ a ¯ • dany jest zbiór nazw komplementarnych (ko-nazw) A, ¯, ¯b, c¯, . . . ∈ A; ¯ l, l0 , ¯l ∈ L; • L jest zbiorem etykiet, L = A ∪ A, • ∀l ∈ L ¯l = l; • Act = L ∪ {τ }, α, β, γ, . . . ∈ Act jest zbiorem zdarzeń (akcji); • τ jest zdarzeniem nieobserwowalnym i nie posiada zdarzenia komplementarnego; • K jest zbiorem stałych agentowych (nazw agentów), A, B, C, · · · ∈ K. 21.

(22) Definicja 1. Zbiór wszystkich wyraz˙eń algebraicznych E rachunku elementarnego CCS definiowany jest indukcyjnie zgodnie z nast˛epujacymi ˛ regułami konstrukcji: (1) Agent pusty 0 jest wyraz˙ eniem algebraicznym. (2) Kaz˙ dy element zbioru K jest wyraz˙ eniem algebraicznym. (3) Jez˙ eli E jest wyraz˙ eniem algebraicznym, to równiez˙ (E), α.E, E[f ] i E\L sa˛ wyraz˙ eniami algebraicznymi, gdzie: • α ∈ Act, • f : Act → Act jest funkcja˛ przeetykietowujac ˛ a˛ spełniajac ˛ a˛ warunki: f (τ ) = τ, f (¯ a) = f (a) dla dowolnej etykiety a ∈ L.. (3.1) (3.2). • L ⊂ L. (4) Jez˙ eli E1 , E2 sa˛ wyraz˙ eniami algebraicznymi, to równiez˙ E1 + E2 i E1 |E2 sa˛ wyraz˙ eniami algebraicznymi. Dla dowolnego modelu w j˛ezyku elementarnym CCS wymagane jest, aby kaz˙ dy agent A z tego modelu był zdefiniowany dokładnie jednym równaniem postaci A = E, gdzie E jest wyraz˙ eniem algebraicznym. Agent pusty 0 jest agentem, który nie moz˙ e wykonać z˙ adnej akcji (nie moz˙ na definiować agenta pustego). Dopuszczalne jest aby definicje były wzajemnie rekurencyjne. Znaczenie operatorów wyst˛epujacych ˛ w definicji 1 jest nast˛epujace: ˛ Operator prefiks (kropka) okre´sla kolejno´sc´ wykonywania akcji, np. agent zdefiniowany wyraz˙ eniem α.A najpierw wykonuje akcj˛e α, a pó´zniej zachowuje si˛e zgodnie z definicja˛ agenta A. Operator sumy (wyboru) + pozwala na wybranie jednej z kilku moz˙ liwych akcji, np. agent zdefiniowany wyraz˙ eniem α.A + β.B najpierw wykonuje akcj˛e α, a pó´zniej zachowuje si˛e zgodnie z definicja˛ agenta A lub najpierw wykonuje akcj˛e β, a pó´zniej zachowuje si˛e zgodnie z definicja˛ agenta B. Operator zło˙zenia równoległego | pozwala łaczy´ ˛ c ze soba˛ agenty. Połaczone ˛ agenty moga˛ komunikować si˛e ze soba,˛ jez˙ eli istnieja˛ pary portów komplementarnych lub funkcjonować niezalez˙ nie od siebie. Operator obci˛ecia \ pozwala ukryć wskazane porty przed otoczeniem. Obci˛ete porty moga˛ być uz˙ ywane wyłacznie ˛ do komunikacji wewn˛etrznej mi˛edzy agentami. Operator przeetykietowania [ ] słuz˙ y do zmiany nazw portów agentów. Stosuje si˛e go w celu uzyskania pary portów komplementarnych, lub wyeliminowania takiej pary, je´sli istnieje, a jest niepoz˙ adana. ˛ Warto ponadto zwrócić uwag˛e, z˙ P e poza operatorem + rozwaz˙ any jest równiez˙ uogólniony operator sumy oznaczany symbolem . (5) Jez˙ eli Ei sa˛ wyraz˙ eniami algebraicznymi dla dowolnego i ∈ I, gdzie I jest przeliczalnym P zbiorem indeksów, to równiez˙ i∈I Ei jest wyraz˙ eniem algebraicznym. 22.

(23) Stosujac ˛ uogólniony operator sumy moz˙ na podać definicj˛e agenta pustego: X 0= Ei .. (3.3). i∈∅. Priorytety dla poszczególnych operatorów sa˛ nast˛epujace ˛ (poczawszy ˛ od najwyz˙ szego): • obci˛ecie \L i przeetykietowanie [f ], • prefiks α., • złoz˙ enie równoległe | , • suma + . Do formalnego przedstawienia omawianego rachunku procesów stosuje si˛e etykietowany system przej´sc´ . a. Definicja 2. Etykietowanym systemem przej´sc´ nazywamy trójk˛e (P roc, Act, {→ − : a ∈ Act}), a gdzie P roc jest zbiorem stanów, Act jest zbiorem akcji, za´s → − ⊆ P roc × P roc jest relacja˛ przej´scia. W odniesieniu do rachunku elementarnego CCS: P roc jest toz˙ samy ze zbiorem wszystkich a wyraz˙ eń agentowych E, zbiór akcji pokrywa si˛e ze zbiorem zdarzeń, a relacja → − jest zdefiniowana dla takich par wyraz˙ eń agentowych E1 , E2 , dla których istnieje α ∈ Act takie, z˙ e α E1 − → E2 . Semantyk˛e j˛ezyka E definiuja˛ reguły tranzycji. Niech E, E 0 , F, F 0 ∈ E oraz niech α ∈ Act i a ∈ L: Pref :. (3.4a). α. Sum1 :. α.E − →E α E− → E0. Sum2 : Com1 :. α. (3.4b). α. (3.4c). E+F − → E0 α F − → F0 E+F − → F0 α E− → E0. (3.4d). α. E|F − → E0 | F α. Com2 :. F − → F0 a. Com3 :. (3.4e). α. → E | F0 E|F − a ¯. E→ − E 0, F → − F0. (3.4f). τ. E|F → − E0 | F 0 α. Res :. E− → E0 α. E\L − → E 0 \L. gdzie α, α ¯∈ /L. (3.4g). α. E− → E0. Rel :. (3.4h). f (α). E[f ] −−→ E 0 [f ] α. Con1 : Con2 :. E− → E0 α. E0. A− → α E− → E0 α. E− →A. def. , gdzie A = E def. , gdzie A = E 0. (3.4i) (3.4j) 23.

(24) α. Brac1 :. E− → E0 α. (E) − → E0. (E ≡ E1 + E2 ). (3.4k). α. Brac2 :. E− → E0 α. (E) − → (E 0 ). (E ≡ E1 | E2 ). (3.4l). Pierwsza reguła (3.4a) dotyczy akcji. Nie posiada ona z˙ adnych prewarunków. Zgodnie z ta˛ reguła˛ proces postaci α.P moz˙ e wykonać akcj˛e α bez dowodzenia wcze´sniej z˙ adnych własno´sci. Przykładowo wyz˙ ej wspomniana reguła pozwala dowie´sc´ prawdziwo´sci nast˛epujacej ˛ tranzycji: in → out.Buff (3.5) in.out.Buff − Reguły (3.4b) i (3.4c) okre´slaja˛ w jaki sposób zachowuje si˛e operator sumy. Zgodnie z tymi regułami wykonanie akcji w sumie wyraz˙ eń jest moz˙ liwe, je´sli dowolny ze składników moz˙ e wykonać t˛e akcj˛e. Reguły (3.4d)-(3.4f) odnosza˛ si˛e do kompozycji agentów. Pierwsze dwa przypadki okres´laja˛ w jaki sposób zachowuje si˛e złoz˙ enie dwóch agentów w przypadku kiedy, odpowiednio pierwszy lub drugi agent moz˙ e wykonać pewna˛ akcj˛e α i nie dochodzi mi˛edzy nimi do komunikacji. Trzecia reguła reprezentuje przypadek, w którym złoz˙ one agenty posiadaja˛ komplementarne etykiety i oba moga˛ wykonać swoje akcje. Wykonywana jest wtedy akcja τ , reprezentujaca ˛ wewn˛etrzna˛ komunikacj˛e i oba agenty przechodza˛ do nast˛epnych stanów. W pierwszych dwóch przypadkach tylko jeden z nich wykonuje akcj˛e α. Równanie (3.4g) przedstawia reguł˛e odnoszac ˛ a˛ si˛e do operatora restrykcji. Reguła ta zabrania wykonania danej akcji, je´sli znajdzie si˛e ona w zbiorze akcji zabronionych, nawet je´sli agent bez restrykcji mógłby wykonać takie przej´scie. Rozwaz˙ my nast˛epujacy ˛ przykład: A = a.b.c.A B = A\{c}. (3.6a) (3.6b). Agent A (3.6a) cyklicznie wykonuje akcje a, b i c. Agent B (3.6b) zdefiniowany jest z wykorzystaniem stałej agentowej (3.4i). Jedynym co go róz˙ ni od agenta A jest umieszczenie etykiety c w zbiorze etykiet zabronionych. Zachowanie obu agentów przedstawia rys. 3.1. Agent B po wykonaniu akcji a i b nie moz˙ e wykonać akcji c i kończy swoja˛ prac˛e. A. a. b.c.A. b. c.A. B. a. b.c.B b. c.B. c. Rys. 3.1. Grafy pochodnych agentów A i B. Reguła (3.4h) opisuje operacj˛e reetykietowania agenta. Pozwala ona na podmian˛e wybranych etykiet na inne. Niech agent A b˛edzie zdefiniowany nast˛epujaco: ˛ A = (a.b.A)[x/a]. (3.7). Zapis taki (3.7) powoduje, z˙ e w definicji agenta A wszystkie wystapienia ˛ etykiety a zostana˛ zastapione ˛ przez etykiet˛e x. Stad ˛ pierwsza˛ akcja˛ wykonana˛ przez tak zdefiniowanego agenta b˛edzie x. Reguły (3.4i) i (3.4j) odnosza˛ si˛e do uz˙ ycia stałych agentowych w opisie. Natomiast reguły (3.4k) i (3.4l) pokazuja˛ semantyk˛e uz˙ ycia nawiasów, odpowiednio dla agenta, który jest suma˛ agentów składowych oraz takiego, który jest złoz˙ eniem innych agentów. 24.

(25) W przykładzie (3.8) pokazano w jaki sposób reguły semantyczne j˛ezyka stosowane sa˛ w praktyce. Przedstawiono krok po kroku, z powołaniem si˛e na wykorzystanie wła´sciwych reguł, w jaki sposób modyfikowane sa˛ wyraz˙ enia opisujace ˛ agentów. A = a.b.A + a.b.0 B = b.a.B + b.B C = (A | B)\{a}. (3.8a) (3.8b) (3.8c). Niech agent C b˛edzie głównym wyraz˙ eniem reprezentujacym ˛ system. Pierwsza˛ operacja˛ b˛edzie rozwini˛ecie stałej agentowej (3.4i). Agent C przyjmie wtedy nast˛epujac ˛ a˛ postać: C = (a.b.A + a.b.0 | b.a.B + b.B)\{a}. (3.9). W dalszej cz˛esći przykładu w celu uproszczenia zapisu i poprawy czytelno´sci tam gdzie b˛edzie to moz˙ liwe lub wygodne b˛eda˛ wstawiane stałe agentowe. Post˛epujac ˛ według kolejno´sci stosowania operatorów w pierwszym rz˛edzie nalez˙ y zastosować operator restrykcji (3.4g). W tym konkretnym przypadku wynika z niego, z˙ e akcje a sa˛ zabronione, czyli cała lewa strona operatora | jest wyłaczona. ˛ Po prawej stronie operatora złoz˙ enia oba składniki sumy moga˛ wykonać odpowiednio akcje b i b. Moz˙ na to wywnioskować posługujac ˛ si˛e kolejno regułami: (3.4a), (3.4e) i (3.4b). W zalez˙ no´sci od wybranej tranzycji agent przejdzie do stanu przedstawionego równaniem (3.10a) lub (3.10b). b. → − (A | a.B)\{a} b. → − (A | B)\{a}. (3.10a) (3.10b). Mogło by si˛e wydawać, z˙ e stan (A | B)\{a} (3.10b) jest identyczny ze stanem C, ale z punktu widzenia grafu pochodnych sa˛ to dwa odr˛ebne w˛ezły, pomimo z˙ e akcje jakie moga˛ wykonać te agenty si˛e pokrywaja.˛ Wnioskowanie jakie nalez˙ y przeprowadzić dla wyraz˙ enia (3.10b) pokrywa si˛e z tym przedstawionym wcze´sniej dla (3.9). Agent ten moz˙ e wykonać akcje b lub b i po ich wykonaniu znajdzie si˛e w stanie opisywanym odpowiednio przez (3.10a) lub (3.10b). Wynika z tego, z˙ e agent (3.10b) po wykonaniu akcji b nie zmienia swojej postaci. Na grafie pochodnych agenta (rys. 3.2) reprezentowane to jest przez p˛etl˛e umieszczona˛ przy odpowiednim w˛ez´ le. Agent (3.10a) moz˙ e wykonać tylko jedna˛ akcj˛e i jest to tzw. akcja wewn˛etrzna – τ . Pomimo, z˙ e operator restrykcji zabrania wykonywania akcji a i a to w tym miejscu on nie działa. Dzieje si˛e tak dlatego, z˙ e do udowodnienia tego przej´scia nalez˙ y zastosować reguły: (3.4a), (3.4b) i reguł˛e (3.4f), która jest kluczowa w tym przypadku. Według niej, jez˙ eli dwóch agentów podlegajacych ˛ operatorowi złoz˙ enia wykonuja˛ w tym samym czasie akcje komplementarne (jeden akcj˛e, drugi ko-akcj˛e) to akcj˛e taka˛ etykietuje si˛e τ . Stad ˛ operator restrykcji odnoszacy ˛ si˛e do akcji a nie ma tu zastosowania. Finalnie agent (3.10a) przechodzi w stan (3.11). τ. → − (b.A | B)\{a}. (3.11). Agent (3.11) ma moz˙ liwo´sc´ wykonania az˙ czterech akcji: τ , podwójnie b oraz b. Operacja τ wynika z obecno´sci akcji komplementarnych (b i b) w wyraz˙ eniu po prawej stronie operatora złoz˙ enia oraz w pierwszym członie sumy po lewej jego stronie. Uzasadnienie dla operatorów sumy i prefiksu jest analogiczne jak w poprzednich przypadkach i b˛edzie tu pomini˛ete. Po uruchomieniu tej akcji agent przejdzie w stan (3.10a). Pierwsza akcja b jest zwiazana ˛ z etykieta˛ po lewej stronie operatora złoz˙ enia i opiera si˛e na (3.4d), a rezultatem jej wykonania jest przej´scie 25.

(26) w stan (3.10b). Druga z akcji b wynika z drugiego członu sumy po prawej stronie operatora złoz˙ enia i moz˙ na ja˛ udowodnić przez (3.4e). Jej wykonanie nie przynosi zmiany stanu agenta. Ostatnia˛ z moz˙ liwych akcji do wykonania w tym stanie jest b. Jej uzasadnienie wynika jak poprzednio z (3.4e) i uwzgl˛ednienia tym razem pierwszego członu sumy po prawej stronie operatora złoz˙ enia. Jej efektem jest przej´scie agenta w stan (3.12). b. → − (b.A | a.B)\{a}. (3.12). W stanie (3.12) agent moz˙ e wykonać tylko operacj˛e b. Moz˙ na ja˛ udowodnić stosujac: ˛ (3.4a) oraz (3.4e). Po wykonaniu akcji b agent znajdzie si˛e w opisywanym juz˙ stanie (3.10a). Kompletny graf pochodnych rozwaz˙ anego agenta znajduje si˛e na rys. 3.2. b. C. (A | B)\{a}. b. b. b. b. (A | a.B)\{a}. τ. (b.A | B)\{a}. b. b. b (b.A | a.B)\{a}. Rys. 3.2. Graf pochodnych agenta C. W monografii [57] zaproponowano wizualizacj˛e procesów, która jest konstruowana na podstawie algebraicznego modelu. Symbol reprezentujacy ˛ pojedynczego agenta pokazano na rys. 3.3. Wewnatrz ˛ owalu reprezentujacego ˛ proces umieszczono jego nazw˛e, za´s poszczególne porty sa˛ oznaczane przez czarne koła rozmieszczo ne na brzegu owalu.. coffee. CS. pub. coin Rys. 3.3. Graficzna reprezentacja procesu w CCS. Tak opracowana reprezentacja graficzna, nawet w przypadku pojedynczego agenta, nie stanowi kompletnego modelu. Przedstawia ona jedynie jego struktur˛e, tj. zawiera nazw˛e agenta i nazwy wszystkich jego portów i pełni wyłacznie ˛ funkcj˛e pomocnicza.˛ Warto podkre´slić, z˙ e nie stanowi ona graficznego j˛ezyka modelowania lecz raczej form˛e pomocnicza˛ w dokumentowaniu opracowanego modelu. Poniz˙ ej znajduje si˛e model pi˛eciu filozofów zapisany zgodnie z formatem akceptowalnym przez CWB. W modelu tym pi˛eciu filozofów siedzi przy wspólnym stole i je z talerza znajdu˙ jacego ˛ si˛e na jego s´rodku. Filozofowie naprzemiennie jedza˛ i my´sla.˛ Zeby je´sc´ kaz˙ dy z nich 26.

(27) a. b b. b. A. B a. a. Rys. 3.4. Graficzna reprezentacja procesu C. agent Fork = up.down.Fork; agent Phil = ’lup.’rup.’ldown.’rdown.Phil; agent agent agent agent agent. Phil1 Phil2 Phil3 Phil4 Phil5. = = = = =. Phil[’u12/’lup,’u51/’rup,’d12/’ldown,’d51/’rdown]; Phil[’u23/’lup,’u12/’rup,’d23/’ldown,’d12/’rdown]; Phil[’u34/’lup,’u23/’rup,’d34/’ldown,’d23/’rdown]; Phil[’u45/’lup,’u34/’rup,’d45/’ldown,’d34/’rdown]; Phil[’u51/’lup,’u45/’rup,’d51/’ldown,’d45/’rdown];. agent agent agent agent agent. Fork1 Fork2 Fork3 Fork4 Fork5. = = = = =. Fork[u12/up,d12/down]; Fork[u23/up,d23/down]; Fork[u34/up,d34/down]; Fork[u45/up,d45/down]; Fork[u51/up,d51/down];. set Res = {u12,u23,u34,u45,u51,d12,d23,d34,d45,d51}; agent S = (Phil1|Phil2|Phil3|Phil4|Phil5| Fork1|Fork2|Fork3|Fork4|Fork5)\Res; Listing 3.1. Model pi˛eciu filozofów dla CWB. potrzebuje podnie´sc´ dwa widelce, które lez˙ a˛ najbliz˙ ej. Widelców jest tylko pi˛ec´ , stad ˛ filozofowie współdziela˛ je z sasiadami. ˛ W prezentowanym przykładzie (listing 3.1) agenty Phil i Fork nie wchodza˛ bezpo´srednio w skład modelowanego systemu. Sa˛ one jedynie rodzajem prototypów, które po wykonaniu odpowiednich operacji reetykietowania, pozwalaja˛ na zbudowanie wła´sciwych agentów Phil1-Phil5 oraz Fork1-Fork5. Z opisu systemu jaki przedstawia listing skryptu dla CWB niezwykle trudno zorientować si˛e jak wyglada ˛ jego struktura i w jaki sposób nast˛epuje komunikacja mi˛edzy agentami.. 3.2. Rozszerzenie czasowe TCCS J˛ezyk TCCS (Timed CCS [26, 57]) jest czasowym rozszerzeniem algebry CCS, przeznaczonym do modelowania systemów współbiez˙ nych z czasem. W porównaniu do prezentowanego w poprzednim podrozdziale elementarnego rachunku CCS, w j˛ezyku TCCS wprowadzono dodatkowy typ akcji, które modeluja˛ upływ czasu. Opisujac ˛ dynamik˛e agenta w algebrze TCCS ˙ mozna wskazać ile jednostek czasu musi odczekać agent przed wykonaniem wskazanej akcji. Dost˛epny jest równiez˙ operator umoz˙ liwiajacy ˛ definiowanie nieograniczonych opó´znień. 27.

(28) Opó´znienia czasowe zapisywane sa˛ podobnie jak akcje z uz˙ yciem operatora prefiks, przy czym do ich oznaczenia stosowane sa˛ liczby naturalne, na przykład agent A = a.4.b.A po wykonaniu akcji a zostaje opó´zniony o cztery jednostki czasu przed wykonaniem akcji b. Nieokre´slone opó´znienie agenta przed wykonaniem danej akcji jest oznaczane przez podkre´slenie odpowiedniej etykiety, np. agent A zdefiniowany równaniem A = a.4.b.A moz˙ e czekać dowolnie długo przed wykonaniem akcji a. W narz˛edziach komputerowych wspierajacych ˛ modelowanie z uz˙ yciem algebry procesów TCCS, zamiast podkre´slenia stosowany jest operator $ umieszczany przed nazwa˛ akcji. Wersja ta b˛edzie stosowana w niniejszej pracy. W porównaniu z j˛ezykiem CCS, w TCCS dost˛epne sa˛ dodatkowo dwa operatory: Operator silnej sumy ++ ma podobne znaczenie jak opisany wcze´sniej operator (słabej) sumy +. Róz˙ nica mi˛edzy tymi operatorami dotyczy sposobu traktowania opó´znień czasowych. Rozwaz˙ my dwa agenty A = 5.a.A + 7.b.A i B = 5.a.B ++7.b.B. W przypadku agenta A moz˙ liwe jest opó´znienie wynoszace ˛ siedem jednostek czasu i wykonanie akcji b. W przypadku agenta B po opó´znieniu wynoszacym ˛ pi˛ec´ jednostek czasu wymuszone zostanie wykonanie akcji a. W efekcie agent ten zachowuje si˛e jak agent zdefiniowany równaniem B = 5.a.B. Operator opó´znienia $ wskazuje na akcje, przed wykonaniem których moz˙ liwe jest nieograniczone opó´znienie. Podobnie jak w przypadku rachunku CCS, moz˙ na podać definicj˛e zbioru wyraz˙ eń algebraicznych E dla rachunku TCCS. Definicja 3. Zbiór wszystkich wyraz˙eń algebraicznych E T rachunku elementarnego TCCS definiowany jest indukcyjnie zgodnie z nast˛epujacymi ˛ regułami konstrukcji: (1) Reguły konstrukcji (1)-(3) z def. 1. (2) Jez˙ eli σ ∈ N+ to σ.E jest wyraz˙ eniem algebraicznym. (3) Jez˙ eli E1 , E2 sa˛ wyraz˙ eniami algebraicznymi, to równiez˙ E1 + E2 , E1 ++E2 i E1 |E2 sa˛ wyraz˙ eniami algebraicznymi. (4) Jez˙ eli E jest wyraz˙ eniem algebraicznym i α ∈ Act, to równiez˙ $α.E jest wyraz˙ eniem algebraicznym. Ponadto tak jak w przypadku algebry CCS, moz˙ na rozwaz˙ ać równiez˙ uogólniona˛ sum˛e dla operatora silnej sumy. Do formalnego przedstawienia rachunku TCCS stosuje si˛e etykietowany system przej´sc´ , podobnie jak dla CCS. Semantyk˛e j˛ezyka E T definiuja˛ reguły tranzycji. Obowiazuj ˛ a˛ tu wszyst1 kie reguły zdefiniowane dla rachunku CCS (zob. wzór (3.4)) . Ponadto konieczne jest wprowadzenie reguł dla nowych operatorów oraz opisania zmian b˛edacych ˛ skutkiem upływu czasu (3.13). 1. 28. przy załoz˙ eniu, z˙ e E, E 0 , F, F 0 ∈ E T.

(29) Niech E, E 0 , F, F 0 ∈ E T i niech α ∈ Act oraz t, s ∈ N+ : α. Sum3 : Sum4 :. E− → E0. s. E. E0. (3.13f). $0 (3.13h). t. $α.E $α.E t 0 E E , ¬F ↑ t t. (3.13i). t. (3.13j). E+F E0 t F F 0 , ¬E ↑ t E+F F0 t t E E 0, F F0. (3.13k). t. E+F E0 + F 0 t t E E 0, F F0 t. E ++F E 0 ++F 0 t t E E 0, F F0 t. E|F E. TRes :. E\L E. TRel :. E[f ] TCon :. (3.13e). E0. (3.13g). t. Idle3 :. TCom :. (3.13d). (t).E. α. $0. TSSum :. s. $α.E − →E. Idle2 :. TWSum3 :. E. s+t. (t).E. TWSum2 :. (3.13b). (s + t).E. Time3 :. TWSum1 :. α. (3.13c). t. (t).E. Idle1 :. (3.13a). E ++F − → F0. Time1 : Time2 :. α. E ++F − → E0 α F − → F0. E A. t t. E 0 |F 0. t. E0. t. E 0 \L. t. E0. t. E 0 [f ]. E0 E0. (3.13l) (3.13m) (3.13n) (3.13o). df. , gdzie A = E. (3.13p). Reguły (3.13a) i (3.13b) okre´slaja˛ zachowanie operatora ++ w przypadku kiedy nie rozpatruje si˛e czasu. Wynika z nich, z˙ e w takiej sytuacji operatory + i ++ zachowuja˛ si˛e identycznie. Równania od (3.13c) do (3.13e) definiuja˛ upływ czasu. Pierwsza z tych reguł przedstawia najprostszy wariant upływu czasu. Agent jest opó´zniony o t jednostek i wykonywane jest przej´scie czasowe o t jednostek. W takim przypadku agent przejdzie do nast˛epnej akcji. Drugie równanie (3.13d) okre´sla moz˙ liwo´sc´ wykonania czastkowego ˛ opó´znienia. Agent opó´zniony 29.

(30) o s + t jednostek wykonuje opó´znienie o s jednostek i dalej oczekuje t jednostek czasu. Ostatni z tych wzorów pokazuje w jaki sposób sumuja˛ si˛e opó´znienia. Agent opó´zniony o s jednostek czasowych i opó´zniony o t jednostek czasowych moz˙ e wykonać przej´scie czasowe o s + t jednostek czasowych. Reguły od (3.13f) do (3.13h) pokazuja˛ semantyk˛e akcji, która moz˙ e być dowolnie opó´zniona (w zapisie akcja poprzedzona operatorem $). Kolejno pokazuja˛ one, z˙ e akcja taka moz˙ e być wykonana bez upływu czasu, agent $0 moz˙ e wykonać dowolne opó´znienie i agent $α.E równiez˙ moz˙ e wykonać dowolne opó´znienie. Reguły od (3.13i) do (3.13k) okre´slaja˛ zachowanie słabej sumy w kontek´scie czasu. Zapis E ↑ t oznacza, z˙ e agent E moz˙ e wykonać opó´znienie t. Równania (3.13i) i (3.13j) pokazuja˛ zachowanie agentów w wypadku kiedy tylko jeden ze składników sumy moz˙ e wykonać opó´znienie. Równanie (3.13k) dotyczy przypadku kiedy oba agenty b˛edace ˛ składnikami sumy sa˛ zdolne do wykonania opó´znienia. Równanie (3.13l) pokazuje semantyk˛e operatora silnej sumy. Operator ten pozwala na wykonanie opó´znienia, tylko je´sli wszystkie składniki takiej sumy sa˛ zdolne do wykonania opó´znienia czasowego. Reguła (3.13m) definiuje zachowanie agentów przy złoz˙ eniu w trakcie wykonywania opó´znienia. Warunkiem wykonania opó´znienia przez złoz˙ onych agentów jest to by kaz˙ dy z nich mógł wykonać opó´znienie. Dalsze reguły definiuja˛ kolejno: restrykcj˛e, reetykietowanie i stała˛ agentowa˛ w kontek´scie czasu. Operatory restrykcji i reetykietowania sa˛ praktycznie transparentne dla tego parametru. Natomiast w wypadku stałej agentowej wymagane jest aby oba agenty zachowywały si˛e identycznie równiez˙ w kwestii przej´sc´ czasowych. Równanie (3.14) pokazuje przykład prostego systemu zbudowanego w oparciu o algebr˛e TCCS. W przykładzie wykorzystano operator silnej sumy, akcje czasowe oraz operator opó´znienia. Rysunek 3.5 przedstawia graf pochodnych agenta C, który w tym przykładzie definiuje system. A = b.1.A ++ $a.A B = 1.a.B + $a.B C = (A | B)\{a}. b. (A | ($a.B + a.B))\{a}. (1.A | ($a.B + a.B))\{a} 1. 1. (A | $a.B)\{a} (1.A | $a.B)\{a} b. b. τ. τ (A | B)\{a}. Rys. 3.5. Graf pochodnych agenta C. 30. b. τ. (1.A | B)\{a}. C. (3.14). 1 τ.