Index of /rozprawy2/10690

Pełen tekst

(1)Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie Wydział Elektrotechniki, Automatyki, Informatyki i In˙zynierii Biomedycznej K ATEDRA I NFORMATYKI S TOSOWANEJ. ROZPRAWA DOKTORSKA. MGR. K RZYSZTOF BALICKI. F ORMALNY OPIS WIZUALNEJ ALGEBRY PROCESÓW XCCS. P ROMOTOR : dr hab. Marcin Szpyrka, prof. AGH. Kraków 2013.

(2) AGH University of Science and Technology in Krakow Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering D EPARTMENT OF A PPLIED C OMPUTER S CIENCE. P H D T HESIS. MGR. K RZYSZTOF BALICKI. F ORMAL DESCRIPTION OF VISUAL PROCESS ALGEBRA XCCS. S UPERVISOR : Marcin Szpyrka, Ph.D. Krakow 2013.

(3) Składam serdeczne podzi˛ekowania Panu prof. Marcinowi Szpyrce za pomoc, której udzielił mi w trakcie pisania rozprawy doktorskiej..

(4) Spis tre´sci. 1. Wprowadzenie......................................................................................................................... 7. 1.1.. Przedstawienie problemu................................................................................................ 8. 1.2.. Cel badań i teza pracy..................................................................................................... 9. 1.3.. Zawarto´sc´ pracy............................................................................................................. 10. 2. Algebra CCS........................................................................................................................... 12 2.1.. Formalna definicja algebry procesów CCS ................................................................... 12. 2.2.. Etykietowane systemy przej´sc´ ....................................................................................... 15. 2.3.. Drzewa dowodzenia....................................................................................................... 16. 2.4.. Przykłady modeli w j˛ezyku CCS................................................................................... 18. 2.5.. Podsumowanie............................................................................................................... 25. 3. Algebra XCCS........................................................................................................................ 26 3.1.. Charakterystyka j˛ezyka XCSS ...................................................................................... 26. 3.2.. Formalna definicja algebry procesów CSS.................................................................... 27. 3.3.. Wprowadzenie do algebry procesów XCCS ................................................................. 29. 3.4.. Formalna definicja algebry procesów XCCS ................................................................ 32. 3.5.. Relacja synchronizacji................................................................................................... 35. 3.6.. Definicje pomocnicze .................................................................................................... 36. 3.7.. Płaskie diagramy XCCS ................................................................................................ 39. 3.8.. Przykłady modeli w j˛ezyku XCCS................................................................................ 39. 3.9.. Konwersja diagramów XCCS do algebr CCS ............................................................... 44. 3.10. Podsumowanie............................................................................................................... 57 4. Modelowanie z u˙zyciem tagów.............................................................................................. 58 4.1.. Wprowadzenie do koncepcji tagów............................................................................... 59. 4.2.. Formalna definicja modeli z tagami .............................................................................. 67. 4.3.. Przykłady diagramów i skryptów XCCS ...................................................................... 70. 4.4.. Konwersja diagramów XCCS do algebr XCCS ............................................................ 72. 4.5.. Semi-graficzna symulacja modeli XCCS ...................................................................... 78. 4.6.. Podsumowanie............................................................................................................... 81 5.

(5) ´ SPIS TRESCI. 6. 5. Weryfikacja modelowa z u˙zyciem CADP evaluator ............................................................ 82 5.1.. Logika modalna µ.......................................................................................................... 82. 5.2.. Przykłady weryfikacji modeli XCCS z uz˙ yciem CADP ............................................... 88. 5.3.. Podsumowanie............................................................................................................... 100. 6. Podsumowanie........................................................................................................................ 101 6.1.. Wnioski końcowe .......................................................................................................... 101. 6.2.. Perspektywy dalszych badań ......................................................................................... 103. K. Balicki Formalny opis (...) algebry procesów XCCS.

(6) 1. Wprowadzenie. Trudno jest współcze´snie wskazać dziedzin˛e działalno´sci człowieka, która nie korzystałaby z róz˙ nego rodzaju systemów informatycznych. Zakres zastosowań systemów informatycznych bardzo dynamicznie si˛e rozszerza i co raz cz˛esćiej stawiane sa˛ pozornie sprzeczne z˙ adania, ˛ aby systemy informatyczne były rozwijane szybko i jednocze´snie charakteryzowały si˛e wysoka˛ niezawodno´scia˛ działania. W wielu bardziej istotny jest brak bł˛edów w systemie informatycznym, niz˙ jego wydajno´sc´ . Przykładem sa˛ chociaz˙ by systemy krytyczne ze wzgl˛edu na bezpieczeństwo (ang. safety critical systems). Termin ten odnosi si˛e do systemów, których bł˛edy działania moga˛ spowodować istotne straty ekonomiczne, uszkodzenia fizyczne czy tez˙ moga˛ mieć wpływ na zdrowie lub z˙ ycie ludzi oraz na s´rodowisko naturalne [41], [42], [43], [44]. Wiele z tych systemów charakteryzuje si˛e współbiez˙ no´scia˛ lub niedeterminizmem działania co powoduje, z˙ e ich weryfikacja z uz˙ yciem standardowych technik takich jak statyczna analiza kodu, czy tez˙ testowanie cz˛esto jest niewystarczajace. ˛ W przypadku systemów, co do których zwi˛ekszone sa˛ oczekiwania odnoszace ˛ si˛e do ich niezawodno´sci, nie moz˙ na odkładać weryfikacji poprawnosći wytwarzanego oprogramowania do etapu testów poszczególnych modułów lub cało´sci systemu. Konieczne wydaje si˛e tutaj wsparcie procesu wytwarzania oprogramowania przez narz˛edzia umoz˙ liwiajace ˛ analiz˛e poprawno´sci rozwijanego systemu juz˙ na poczatkowych ˛ etapach jego powstawania. Dołaczenie ˛ do procesu wytwarzania oprogramowania metod formalnych moz˙ e nie tylko znaczaco ˛ zwi˛ekszyć prawdopodobieństwo uzyskania poprawnego systemu, ale takz˙ e obniz˙ yć koszty jego wytworzenia oraz skrócić czas potrzebny na wytworzenie systemu. Waz˙ ny jest tutaj równiez˙ czynnik finansowy. Koszty usuwania bł˛edów znaczaco ˛ wzrastaja˛ (nawet 500 razy) wraz z przechodzeniem do kolejnych etapów wytwarzania oprogramowania [42]. Terminem metody formalne okre´sla si˛e bazujace ˛ na matematyce podej´scia do specyfikacji, projektowania i weryfikacji systemów informatycznych. Zastosowanie modelu formalnego, który charakteryzuje si˛e jednoznaczna˛ semantyka,˛ pozwala precyzyjnie okre´slić, jakie jest poz˙ adane ˛ działanie systemu (co system informatyczny powinien robić) i jakie maja˛ być jego własno´sci. Zastosowanie metod formalnych w procesie wytwarzania oprogramowania ma juz˙ ok. pi˛ec´ dziesi˛ecioletnia˛ histori˛e, a ponad trzydzie´sci lat trwaja˛ dyskusje nad ich przydatno´scia.˛ Niezalez˙ nie od tego ciagle ˛ rozwijane sa˛ istniejace ˛ podej´scia, a takz˙ e proponuje si˛e nowe metody. Warto tutaj przytoczyć chociaz˙ by dynamicznie rozwijajace ˛ si˛e podej´scia okre´slane mianem weryfikacji modelowej [5], które sa˛ przykładem praktycznego zastosowania logik temporalnych w inz˙ ynierii oprogramowania. W´sród najwaz˙ niejszych współcze´snie grup metod formalnych stosowanych do modelowania i weryfikacji 7.

(7) 1.1. Przedstawienie problemu. 8. systemów wbudowanych moz˙ na wyróz˙ nić: – algebry procesów ([10, 11, 12, 18, 23, 35, 36]), – automaty czasowe ([2, 3, 4, 9]), – logiki temporalne ([13, 28, 30, 31, 38]), – sieci Petriego ([26, 39, 45, 46]). Warto podkre´slić, z˙ e współcze´snie wiele instytucji wskazuje na konieczno´sc´ kształcenia inz˙ ynierów informatyków w zakresie metod formalnych, które sa˛ dla informatyka niezwykle istotna˛ gał˛ezia˛ matematyki stosowanej. Stosowanie metod formalnych bywa równiez˙ narzucane wymaganiami prawnymi, np. przy ocenie bezpieczeństwa systemów teleinformatycznych stosowane sa˛ normy ITSEC (Information Technology Security Evaluation Criteria) i Common Criteria (norma ISO 15408), które w zalez˙ no´sci od poziomu bezpieczeństwa zalecaja˛ lub wymagaja˛ zastosowania metod formalnych.. 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ń. Podstawowym jej celem jest formalne opisanie j˛ezyka modelowania XCCS. J˛ezyk ten jest oparty na algebrach procesów CCS (Calculus of Communicating Systems, [1], [18], [35]), ale rozszerza je o moz˙ liwo´sci wizualnej metody modelowania systemów współbiez˙ nych. J˛ezyk modelowania XCCS (eXtended CCS) charakteryzuje si˛e m.in. nast˛epujacymi ˛ własno´sciami: – Dostarcza graficzna˛ warstw˛e projektowania reprezentujac ˛ a˛ struktur˛e tworzonego systemu. – Wspiera zarówno rachunek elementarny CCS jak i wersj˛e rozszerzona˛ VP CCS. – Przy´spiesza projektowanie systemów współbiez˙ nych z zastosowaniem algebr procesów CCS – łatwe ponowne wykorzystanie zaprojektowanych komponentów, łatwo´sc´ ich łaczenia ˛ itp. – Ogranicza moz˙ liwo´sc´ popełnienia bł˛edów typowych przy pisaniu skryptów CCS – brak oczekiwanych połacze´ ˛ n, wyst˛epowanie połacze´ ˛ n nadmiarowych itp. – Ma moz˙ liwo´sc´ automatycznego uzyskania skryptu w j˛ezyku CCS lub VP CCS na podstawie diagramu XCCS, a co za tym idzie moz˙ liwo´sc´ skorzystania z dost˛epnych narz˛edzi do formalnej weryfikacji systemów opisywanych z uz˙ yciem algebr procesów CCS. – Ma moz˙ liwo´sc´ automatycznego uzyskania reprezentacji w postaci systemu przej´sc´ etykietowanych (LTS), co pozwala na zastosowanie narz˛edzi wspierajacych ˛ weryfikacj˛e takich modeli dla systemów opisanych z uz˙ yciem XCCS. K. Balicki Formalny opis (...) algebry procesów XCCS.

(8) 1.2. Cel badań i teza pracy. 9. Pierwszy etap prac nad rozwojem j˛ezyka XCCS, które prowadzono w Katedrze Automatyki AGH (ówczesny Wydział Elektrotechniki, Automatyki Informatyki i Elektroniki) został podsumowany w rozprawie doktorskiej [33]. W rozprawie przedstawiono algebraiczno-graficzny j˛ezyk modelowania XCCS od strony inz˙ ynierskiej. Omówiono składni˛e j˛ezyka i nieformalnie opisano jego semantyk˛e. W pracy tej nie podj˛eto próby formalnego opisu j˛ezyka XCCS. Skupiono si˛e na próbie pokazania praktycznego aspektu zastosowania wprowadzonego j˛ezyka modelowania. Opisano zaimplementowane narz˛edzia wspierajace ˛ modelowanie z uz˙ yciem XCCS [49] oraz pokazano przykład zastosowania XCCS do modelowania sterowania robotem kroczacym ˛ Hexor II [52]. Podsumowujac ˛ ten okres prac nad j˛ezykiem XCCS moz˙ na powiedzieć, z˙ e moz˙ na go było zaliczyć do metod formalnych dzi˛eki translacji do rachunku CCS. Dla dowolnego modelu XCCS moz˙ na było wygenerować równowaz˙ ny skrypt algebry procesów CCS i do jego weryfikacji zastosować metody dost˛epne dla rachunku CCS. Niniejsza rozprawa opisuje efekty kontynuowania prac nad rozwojem j˛ezyka XCCS. Jak wspomniano, podstawowym celem było opracowanie formalnego opisu tego j˛ezyka. Wyniki prowadzonych prac przedstawiono m.in w publikacjach: [6], [8], [7], [48]. Warto tutaj zwrócić uwag˛e na przedstawiona˛ w rozdziale 4 koncepcj˛e tagów, które sa˛ istotnym nowym elementem wprowadzonym do j˛ezyka XCCS. Pozwalaja˛ one wyeliminować jedna˛ w niedogodno´sci algorytmu translacji z j˛ezyka XCCS do CCS, jaka˛ jest niewatpliwie ˛ automatyczne reetykietowanie portów agentów. W dotychczasowym podej´sciu uz˙ ytkownik nie miał wpływu na metod˛e podmiany nazw portów i w przypadku stwierdzenia bł˛edu na poziomie skryptu CCS, konieczna była manualna analiza wygenerowanego skryptu w celu dopasowania nazw portów na poziomie CCS i XCCS, tak aby moz˙ na było zidentyfikować przyczyn˛e bł˛edu w modelu wyj´sciowym. Zastosowanie tagów pozwala zachować oryginalne etykiety portów, co całkowicie eliminuje opisany problem.. 1.2. Cel badan´ i teza pracy Jako podstawowy cel podj˛etych badań przyj˛eto opracowanie formalnej definicji dla j˛ezyka XCCS. Definicja taka stanowi naturalne uzupełnienie opisu składni XCCS przedstawionej w rozprawie [33]. Pozwala ona równiez˙ na zaliczenie algebry procesów XCCS do metod formalnych bez potrzeby uciekania si˛e do translacji modelu do skryptów CCS. Drugim celem bezpo´srednio powiazanym ˛ z opracowaniem formalnego opisu j˛ezyka XCCS, było dołaczenie ˛ do opisywanego formalizmu koncepcji tagów, tak aby moz˙ na było korzystać z nich jako integralnej cz˛esći tego j˛ezyka. Jak juz˙ wspomniano w poprzednim podrozdziale, pozwalaja˛ one wyeliminować jedna˛ z niedogodno´sci algorytmu translacji z j˛ezyka XCCS do algebr procesów CCS. Jak pokazano w rozprawie, nie jest to ich jedyna zaleta. Znacznie ułatwiaja˛ one generowanie grafów LTS dla modelu, co pokazano w rozdziale 4. J˛ezyk XCCS opracowano w celu ułatwienia modelowania w j˛ezyku zbliz˙ onym do algebr procesów CCS, wyeliminowaniu moz˙ liwo´sci popełniania cz˛esto spotykanych bł˛edów zwiazanych ˛ z uz˙ yciem rachunku CCS, a takz˙ e w celu umoz˙ liwienia modelowania zdecydowanie bardziej złoz˙ onych systemów, niz˙ ma to miejsce w przypadku CCS. To ostatnie załoz˙ enie generuje problemy przy weK. Balicki Formalny opis (...) algebry procesów XCCS.

(9) 1.3. Zawarto´sc´ pracy. 10. ryfikacji złoz˙ onych modeli (o duz˙ ej liczbie stanów) z uz˙ yciem oprogramowania CWB (Edinburgh Concurrency Workbench [37]), które stanowi najpopularniejszy pakiet do implementacji i weryfikacji modeli implementowanych z uz˙ yciem róz˙ nych wersji algebry procesów CCS. Przyj˛eto załoz˙ enie o konieczno´sci opracowania algorytmów generowania grafów LTS (Labelled Transition System) bezpo´srednio z modelu w j˛ezyku XCCS i zastosowaniu bardziej zaawansowanych narz˛edzi do weryfikacji przestrzeni stanów wyraz˙ anych za pomoca˛ grafów LTS. W prezentowanym podej´sciu zdecydowano si˛e na zastosowanie pakietu CADP (Construction and Analysis of Distributed Processes, [20], [21]) rozwijanego przez zespół VASY przy INRIA (l’Institut National de Recherche en Informatique et en Automatique). CADP jest pakietem oferujacym ˛ szeroka˛ gam˛e narz˛edzi, poczawszy ˛ od prostych symulacji krokowych, a skończywszy na weryfikacji modelowej. Pakiet jest oprogramowaniem komercyjnym, ale dla o´srodków akademickich dost˛epna jest darmowa licencja. Pozwala ona pracownikom naukowym i studentom nieodpłatnie korzystać z wszystkich zawartych w pakiecie narz˛edzi. Aktualna wersja pakietu CADP daje moz˙ liwo´sc´ weryfikacji grafów LTS, które zawieraja˛ do 244 elementów. Podsumowujac, ˛ przyj˛ete tezy pracy moz˙ na sći´sle sformułować nast˛epujaco: ˛ Moz˙liwe jest formalne zdefiniowanie algebr procesów XCCS zawierajacych ˛ wizualny j˛ezyk modelowania systemów współbiez˙nych. Dla tak opisanych algebr XCCS moz˙liwa jest ponadto ich formalna analiza z zastosowaniem metod i narz˛edzi typowych dla algebr CCS lub metod bazujacych ˛ na analizie etykietowanych systemów przej´sc´ (LTS).. 1.3. Zawarto´sc´ pracy Pomijajac ˛ Wprowadzenie i Podsumowanie, niniejsza rozprawa została podzielona na cztery rozdziały. Poza rozdziałem 2, który zawiera podstawowe informacje dotyczace ˛ algebry procesów CCS niezb˛edne do omówienia j˛ezyka XCCS, pozostałe rozdziały dotycza˛ wyłacznie ˛ j˛ezyka XCCS. Szczegółowy opis zawarto´sci poszczególnych rozdziałów podano poniz˙ ej. – Rozdział 2 zawiera wprowadzenie do algebry procesów CCS, która posłuz˙ yła za podstaw˛e do opracowania j˛ezyka XCCS. Prezentowany opis algebry CCS został opracowany na podstawie monografii [18]. W rozdziale zawarto: formalna˛ definicj˛e algebry procesów CCS, opisano etykietowane systemy przej´sc´ (grafy LTS), omówiono drzewa dowodzenia oraz podano przykłady modelowania w j˛ezyku CCS. – Rozdział 3 zawiera opis j˛ezyka modelowania XCCS. W rozdziale okre´slono podzbiór algebry CCS o nazwie CSS (z ang. Calculus of Sequential Systems), która słuz˙ y do opisu procesów sekwencyjnych, w sposób formalny zdefiniowano j˛ezyk modelowania XCCS, opisano róz˙ nic˛e mi˛edzy płaskimi i pełnymi diagramami XCCS, zdefiniowano relacj˛e synchronizacji, podano definicje pomocnicze poj˛ec´ zwiazanych ˛ z diagramami XCCS, podano przykłady modeli w postaci diagramów XCCS, w sposób formalny opisano własno´sci konfliktów i zaciemnień dla diagramów XCCS, które daja˛ niepoprawne skrypty CCS przy wykorzystaniu trywialnego K. Balicki Formalny opis (...) algebry procesów XCCS.

(10) 1.3. Zawarto´sc´ pracy. 11. algorytmu konwersji, podano algorytm konwersji płaskich i pełnych diagramów XCCS do algebr procesów CCS wraz z przykładami konwersji. – Rozdział 4 dotyczy modelowania z wykorzystaniem mechanizmu tagów. Opisano w nim dotychczasowy algorytm translacji modeli XCCS do rachunku procesów CCS, omówiono koncepcj˛e tagów, przestawiono formalna˛ definicj˛e j˛ezyka XCCS z tagami, oraz omówiono algorytm konwersji diagramów XCCS do algebr XCCS (j˛ezyk XCCS w wersji czysto algebraicznej). Prezentowane w rozdziale zagadnienia zilustrowano przykładami. Na zakończenie rozdziału omówiono koncepcj˛e semi-graficznej symulacji modeli XCCS. – W rozdziale 5 przedstawiono opis logiki modalnej µ, która jest stosowana do specyfikowania własno´sci systemów na potrzeby programu CADP evaluator oraz przykłady uz˙ ycia weryfikacji modelowej (CADP evaluator) do analizy modelu w j˛ezyku XCCS. Prezentowane w tym rozdziale podej´scie jest alternatywa˛ dla konwersji modeli XCCS do skryptów w rachunku CCS i stosowania pakietu CWB. Zastosowanie pakietu CADP nie tylko pozwala na przetwarzania zdecydowanie wi˛ekszych grafów LTS, ale równiez˙ oferuje znacznie bogatsza˛ palet˛e dost˛epnych metod analizy modeli. – Rozdział 6 zawiera podsumowanie wyników zawartych w rozprawie. Poza wnioskami końcowymi zawarto w nim równiez˙ perspektywy dalszych badań dotyczacych ˛ j˛ezyka XCCS.. K. Balicki Formalny opis (...) algebry procesów XCCS.

(11) 2. Algebra CCS. Termin algebry procesów uz˙ ywany jest w odniesieniu do metod formalnych, w których opis stanów i zachowania si˛e systemu wzorowany jest na rachunku algebraicznym. Pierwsza˛ algebra˛ procesów była zaproponowana przez Charlesa. A. R. Hoare’a w 1978 roku pierwotna wersja algebry CSP (Communicating Sequential Processes), której pełna˛ wersj˛e przedstawiono w pracy [23]. Niezalez˙ nie rozwijana była algebra CCS (Calculus of Communicating Systems) zaproponowana przez Robina Milnera. Jej pierwsza˛ wersj˛e, zawierajac ˛ a˛ odpowiednie definicje i twierdzenia algebraiczne wraz z modelem semantycznym przedstawiono w pracy [34], a ostateczna˛ w monografii [35]. Algebra ta doczekała si˛e równiez˙ innych ciekawych opracowań ksia˛z˙ kowych np. [1] i [18]. Algebry CCS i CSP były podstawa˛ do opracowania przez ISO (International Standards Organization) algebry LOTOS (Language Of Temporal Ordering Specification, [24], [25]). Przykładami innych znanych formalizmów zaliczanych do algebr procesów sa˛ równiez˙ : ACP (Algebra of Communicating Processes, [10]), RSL (Raise Specification Language, [22]) oraz rachunek π (π-calculus, [36]). Przeglad ˛ róz˙ nych formalizmów algebraicznych moz˙ na znale´zc´ w monografii [11]. W niniejszym rozdziale przedstawiona została algebra procesów CCS. W omawianym podejsćiu dynamika modelowanego systemu jest definiowana w postaci ciagu ˛ wyraz˙ eń algebraicznych. Analiza modelu zorientowana jest na akcje wykonywane przez system, w szczególno´sci moz˙ emy rozwaz˙ ać wyłacznie ˛ akcje obserwowane z zewnatrz. ˛ Poniz˙ szy opis algebry CCS został opracowany na podstawie monografii [18]. W pracy tej wyraz˙ enia agentowe zdecydowano si˛e zdefiniować przy pomocy notacji BNF.. 2.1. Formalna definicja algebry procesów CCS Podstawowym poj˛eciem algebry procesów CCS jest agent. Jest to dowolna cz˛esć´ modelowanego systemu, która ma swoja˛ własna˛ toz˙ samo´sc´ trwajac ˛ a˛ w czasie. Biorac ˛ pod uwag˛e, z˙ e skupiamy si˛e wyłacznie ˛ na analizie dynamiki modelowanego systemu, agent cz˛esto jest utoz˙ samiany z procesem. Na agenta moz˙ emy patrzeć jak na czarna˛ skrzynk˛e, która ma swoja˛ nazw˛e i zdefiniowany interfejs do komunikacji z otoczeniem. Interfejs ten jest zbiorem tzw. portów komunikacyjnych. Para portów o komplementarnych (uzupełniajacych ˛ si˛e) etykietach, np. a i a, tworzy kanał komunikacyjny poprzez który dwa agenty moga˛ si˛e komunikować. Pojedyncze porty moga˛ być równiez˙ uz˙ yte do komunikacji z otoczeniem modelowanego systemu. Rachunek CCS dostarcza równiez˙ szereg ope12.

(12) 13. 2.1. Formalna definicja algebry procesów CCS. ratorów, które pozwalaja˛ łaczy´ ˛ c ze soba˛ agenty budujac ˛ w tej sposób agenty (procesy) o bardziej złoz˙ onym zachowaniu i moz˙ liwej komunikacji wewn˛etrznej. Na potrzeby formalnego zdefiniowania algebry CCS przyjmiemy nast˛epujace ˛ oznaczenia: – A jest zbiorem nazw, gdzie a, b, . . . ∈ A. – A jest zbiorem ko-nazw (nazw komplementarnych), gdzie a, b, . . . ∈ A. – L := A ∪ A jest zbiorem etykiet, gdzie l, l0 , . . . ∈ L. – Act := L ∪ {τ } jest zbiorem akcji, gdzie α, β, . . . ∈ Act. – K jest zbiorem stałych agentowych, gdzie A, B, C, . . . ∈ K. – E jest zbiorem wyraz˙ eń agentowych okre´slonych przez nast˛epujac ˛ a˛ notacj˛e BNF: E ::= 0 | A | E[f ] | E\K | (E) | α.E | [E|E] | E + E. (2.1). gdzie K ⊆ L, a priorytet operatorów jest okre´slony w porzadku ˛ malejacym. ˛ Zwróćmy uwag˛e, z˙ e nawiasów kwadratowych [ ] uz˙ ywamy tylko ze wzgl˛edu na podobieństwo operatora złoz˙ enia | do operatora | stosowanego w opisie gramatyk BNF. Dodatkowo zakładamy, z˙ e symbol 0 nie jest zdefiniowany przez z˙ adne równanie, a dla kaz˙ dej def. stałej agentowej A istnieje dokładnie jedno równanie definiujace ˛ postaci A = E, gdzie E jest wyraz˙ eniem zdefiniowanym przez (2.1). Model systemu w postaci algebry CCS najcz˛esćiej okre´sla si˛e przy pomocy ciagu ˛ równań algebraicznych postaci: def. A1 = E1 def. A2 = E2 ... def. An = En Dla wygody przyjmujemy, z˙ e nazwa stałej agentowej A1 w pierwszym równaniu algebraicznym jest nazwa˛ całej algebry CCS. Model systemu w postaci algebry CCS nazywamy równiez˙ : skryptem CCS, programem CCS, CCS modelem lub po prostu algebra˛ CCS. Złoz˙ one systemy współbiez˙ ne moga˛ być postrzegane jako układy (sieci) agentów wzajemnie si˛e ze soba˛ komunikujacych. ˛ W rachunku CCS dynamika złoz˙ onego systemu jest okre´slona poprzez operacje wykonywane przez poszczególnych agentów go tworzacych. ˛ Do opisu systemów złoz˙ onych z wi˛ecej niz˙ jednego agenta uz˙ ywa si˛e pi˛eciu operatorów wskazanych w (2.1): prefiks (.), suma (+), złoz˙enie (|), restrykcja (\) i przeetykietowanie ([]). Ich znaczenie jest nast˛epujace: ˛ Operator prefiks . 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. K. Balicki Formalny opis (...) algebry procesów XCCS.

(13) 14. 2.1. Formalna definicja algebry procesów CCS. Operator sumy (wyboru) + pozwala na wybranie jednej z dwóch 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˛ 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. Komunikacja dwóch agentów jest moz˙ liwa, je´sli istnieje co najmniej jedna para portów (nalez˙ acych ˛ do róz˙ nych agentów) o uzupełniajacych ˛ si˛e etykietach. Jednoczesne wystapienie ˛ akcji reprezentowanych przez takie etykiety oznacza akcj˛e wewn˛etrzna,˛ nieobserwowalna˛ z zewnatrz, ˛ która oznaczana jest litera˛ τ niezalez˙ nie od etykiet połaczonych ˛ portów. Zakładamy, z˙ e w kaz˙ dym kolejnym kroku moz˙ e synchronizować ze soba˛ tylko jedna para akcji komplementarnych. 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.. W algebrze procesów CCS wyraz˙ enia agentowe postaci 2.1 pozwalaja˛ opisać wszystkie moz˙ liwe stany modelowanego systemu. Natomiast zachowanie, czyli dynamik˛e modelowanego systemu okre´sla si˛e przy pomocy strukturalnej semantyki operacyjnej. Podamy teraz zbiór podstawowych reguł przej´sc´ dla alegbry CCS. Niech E, F, E 0 , F 0 ∈ E i niech α ∈ Act i l ∈ L. Semantyka operacyjna j˛ezyka E okre´slona jest przez nast˛epujacy ˛ zbiór reguł przej´sc´ : Pref. α. α.E → E. (2.2a). α. Sum1. E → E0 α. E + F → E0. (2.2b). α. Sum2. F → F0 α. E + F → F0. (2.2c). α. Com1. E → E0 α. E|F → E 0 |F. (2.2d). α. Com2. F → F0 α. E|F → E|F 0. K. Balicki Formalny opis (...) algebry procesów XCCS. (2.2e).

(14) 15. 2.2. Etykietowane systemy przej´sc´. ¯ l. l. Com3. E → E0 F → F 0 τ. E|F → E 0 |F 0. (2.2f). α. Res. E → E0 α. E\L → E 0 \L. (α, α ¯∈ / L). (2.2g). l. Rel. E → E0 f (l). E[f ] →. (2.2h). E 0 [f ]. α. Con1. E → E0 α. E0. A→. def. (A = E). (2.2i). α. Con2. E → E0 α. E→A. def. (A = E 0 ). (2.2j). α. Brac1. E → E0 α. (E) → E 0. (E ≡ E1 + E2 ). (2.2k). (E ≡ E1 |E2 ). (2.2l). α. Brac2. E → E0 α. (E) → (E 0 ). ¯ = a, dla reguły Res zakładamy τ¯ = τ , a w regule Rel symbol gdzie dla reguły Com3 zakładamy a f oznacza funkcj˛e reetykietujaca ˛ f : L → L, która spełnia warunek f (l) = f (l). Wi˛ecej informacji na temat strukturalnej semantyki operacyjnej zawarto w podrozdziale 2.3.. 2.2. Etykietowane systemy przej´sc´ Do formalnego przedstawienia modeli systemów zapisanych w postaci algebr procesów CCS stosuje si˛e etykietowane systemy przej´sc´ . Po zapisaniu w odpowiednim formacie wykorzystuje si˛e je jako dane wej´sciowe dla narz˛edzi sprawdzajacych ˛ własno´sci systemów skończenie stanowych. Definicja 2.1. Etykietowanym systemem przej´sc´ (z ang. Labelled Transition System – LTS) nazywamy trójk˛e (Γ, A, →), gdzie: – Γ jest zbiorem stanów, – A jest zbiorem akcji, – →⊆ Γ × A × Γ jest relacja˛ przej´scia. W odniesieniu do algebry procesów CCS zachodzi: – Γ=E – A = Act def. α. – (E, α, E 0 ) ∈ → ⇐⇒ E → E 0 K. Balicki Formalny opis (...) algebry procesów XCCS.

(15) 16. 2.3. Drzewa dowodzenia. α. Przy czym zapis E → E 0 oznacza, z˙ e tranzycja ze stanu E do stanu E 0 przez wykonanie akcji α jest uprawniona, czyli z˙ e moz˙ na ja˛ udowodnić przy pomocy reguł przej´sc´ podanych w podrozdziale 2.1. Przykłady tego typu dowodów znajduja˛ si˛e w kolejnym podrozdziale. Je´sli dla stanu E i akcji α istnieje tylko jedna trójka (E, α, E 0 ) ∈ → to mówimy, z˙ e akcja α jest deterministyczna dla stanu E. Je´sli dla stanu E i akcji α istnieje przynajmniej jedna trójka (E, α, E 0 ) ∈ → to mówimy, z˙ e akcja α jest wykonywalna dla stanu E. Etykietowany system przej´sc´ moz˙ na przedstawiać jako etykietowany multigraf skierowany. W˛ezły takiego grafu reprezentuja˛ stany systemu. Kraw˛edzie etykietowane nazwami akcji, łacz ˛ ace ˛ poszczególne w˛ezły, reprezentuja˛ przej´scia mi˛edzy odpowiednimi stanami. Dwa w˛ezły moga˛ być połaczone ˛ wi˛ecej niz˙ jedna˛ kraw˛edzia,˛ jez˙ eli wykonanie wi˛ecej niz˙ jednej akcji powoduje takie same zmiany stanów. W zbiorze stanów moz˙ na wyróz˙ nić stan poczatkowy. ˛ W odniesieniu do algebry procesów CCS etykietowane systemy przej´sc´ nazywane sa˛ grafami przej´sc´ lub grafami pochodnych. Przykłady takich grafów zawarto w kolejnych podrozdziałach.. 2.3. Drzewa dowodzenia Strukturalna semantyka operacyjna (z ang. Structural Operational Semantics) została zaproponowana przez G. Plotkina w raporcie technicznym pt. A Structural Approach to Operational Semantics w roku 1981. Wyniki w nim zawarte zostały w pó´zniejszym czasie opublikowane wraz z poprawkami w pracy [40]. Strukturalna semantyka operacyjna jest okre´slona przez zbiór reguł przej´sc´ . Reguły te definiuja˛ tranzycje dla elementarnych wyraz˙ eń składniowych, co z kolei pozwala wydedukować wszystkie moz˙ liwe tranzycje dla złoz˙ onych wyraz˙ eń składniowych. Reguły przej´sc´ maja˛ postać: Reguła. przesłanki (warunki) wniosek. (2.3). Wyja´snimy teraz pokrótce w jaki sposób konstruujemy drzewo dowodu poprawno´sci dla tranzycji w odniesieniu do algebr CCS. Dowodzenie poprawno´sci tranzycji rozpoczynamy zawsze od jednej lub wi˛ecej reguł Pref , jako z˙ e maja˛ one pusty zbiór przesłanek. Na kolejnym poziomie w drzewie dowodu wnioski z reguł wyst˛epujacych ˛ na poprzednim poziomie staja˛ si˛e przesłankami dla reguł na aktualnym poziomie. Podobnie post˛epujemy na kolejnych poziomach. Przy czym, reguły dobieramy w taki sposób, aby na korzeniu drzewa znalazła si˛e reguła, która we wnioskach ma tranzycj˛e, która˛ chcemy udowodnić. Je´sli utworzenie drzewa dowodu dla danej tranzycji jest niemoz˙ liwe, to oznacza to, z˙ e jest ona niewykonywalna. Rozwaz˙ ymy teraz kilka przykładów dowodzenia poprawno´sci wybranych tranzycji w grafach przej´sc´ z kolejnego podrozdziału. Na poczatek ˛ udowodnimy poprawno´sc´ tranzycji z przykładu 2.5: τ. (a.0|a.0)\{a} → (0|0)\{a} K. Balicki Formalny opis (...) algebry procesów XCCS.

(16) 17. 2.3. Drzewa dowodzenia. W rozwaz˙ anym przykładzie drzewo dowodu konstruujemy rozpoczynajac ˛ od dwukrotnego uz˙ ycia reguły Pref . Na drugim poziomie w drzewie dowodu wnioski z reguł Pref podstawiamy do przesłanek w regule Com3 . Na trzecim poziomie w drzewie dowodu wniosek z reguły Com3 podstawiamy do przesłanki w regule Brac2 . Na czwartym poziomie w drzewie dowodu wniosek z reguły Brac2 podstawiamy do przesłanki w regule Res i jak widać we wnioskach dla tej reguły pojawia si˛e tranzycja, która˛ mieli´smy udowodnić. a. a.0 → 0. Pref. a. Pref. a.0 → 0 a. a. a.0 → 0 a.0 → 0. Com3. τ. a.0|a.0 → 0|0 τ. a.0|a.0 → 0|0. Brac2. τ. (a.0|a.0) → (0|0) τ. (a.0|a.0) → (0|0) τ. (a.0|a.0)\{a} → (0|0)\{a}. (τ, τ¯ ∈ / {a}) Res. Jako drugi przykład rozwaz˙ ymy tranzycj˛e z rysunku 2.8: out. (m.C1 |out.C2 )\{m} −→ (m.C1 |C2 )\{m} Tym razem konstrukcj˛e drzewa dowodu rozpoczynamy od pojedynczej reguły Pref. Na drugim poziomie wniosek z tej reguły podstawiamy do przesłanki w regule Com2 . Na trzecim poziomie wniosek z tej reguły podstawiamy do przesłanki w regule Brac2 . Na czwartym ostatnim poziomie wniosek z tej reguły podstawiamy do przesłanki w regule Res i we wnioskach dla tej reguły otrzymujemy tranzycj˛e, która˛ mieli´smy udowodnić. out. Pref. out.C2 −→ C2 out. out.C2 −→ C2. Com2. out. m.C1 |out.C2 −→ m.C1 |C2 out. m.C1 |out.C2 −→ m.C1 |C2. Brac2. out. (m.C1 |out.C2 ) −→ (m.C1 |C2 ) out. (m.C1 |out.C2 ) −→ (m.C1 |C2 ) out. (out, out ∈ / {m}) Res. (m.C1 |out.C2 )\{m} −→ (m.C1 |C2 )\{m} Na rysunku 2.8 poprawna jest równiez˙ tranzycja: τ. (m.C1 |C2 )\{m} −→ (C1 |out.C2 )\{m} W tym przypadku drzewo dowodu rozpoczynamy od dwukrotnego zastosowania reguły Pref . Na drugim poziomie wniosek z reguły, która pojawiła si˛e wcze´sniej po prawej stronie podstawiamy K. Balicki Formalny opis (...) algebry procesów XCCS.

(17) 18. 2.4. Przykłady modeli w j˛ezyku CCS. do przesłanki w regule Con1 . Na trzecim poziomie wniosek z lewej reguły na pierwszym poziomie i wniosek z reguły na drugim poziomie podstawiamy do przesłanek w regule Com3 . Na czwartym poziomie wniosek z tej reguły podstawiamy do przesłanki w regule Brac2 . Na piatym ˛ ostatnim poziomie wniosek z tej reguły podstawiamy do przesłanki w regule Res i we wnioskach dla tej reguły otrzymujemy tranzycj˛e, która˛ mieli´smy udowodnić. m. Pref. m. m.out.C2 −→ out.C2. m.C1 −→ C1. Pref. m. m.out.C2 −→ out.C2 m. C2 −→ out.C2. Con1. m. m. m.C1 −→ C1 C2 −→ out.C2 τ. m.C1 |C2 −→ C1 |out.C2. Com3. τ. m.C1 |C2 −→ C1 |out.C2 τ. (m.C1 |C2 ) −→ (C1 |out.C2 ). (E ≡ E1 |E2 ) Brac2. τ. (m.C1 |C2 ) −→ (C1 |out.C2 ) τ. (m.C1 |C2 )\{m} −→ (C1 |out.C2 )\{m}. (τ, τ ∈ / {m}) Res. 2.4. Przykłady modeli w j˛ezyku CCS W niniejszym podrozdziale przedstawiono kilka przykładów modeli w j˛ezyku CCS. Maja˛ one na celu przybliz˙ yć poszczególne operatory algebry CCS oraz przedstawić metody konstruowania modeli złoz˙ onych w wielu agentów. Przykład 2.1. a.τ.b.0 Agent a.τ.b.0 wykonuje kolejno akcje a, τ , b, po czym staje si˛e agentem martwym 0. Zmiana stanów agenta opisana jest graf przej´sc´ pokazany na rys. 2.1. a. τ. b. a.τ.b.0 −→ τ.b.0 −→ b.0 −→ 0 Rysunek 2.1: Graf przej´sc´ dla przykładu 2.1 Przykład 2.2. a.0 + b.0 Agent a.0 + b.0 przy stanie poczatkowym ˛ moz˙ e wykonać akcj˛e a albo akcj˛e b. Po wykonaniu dowolnej z tych akcji wspomniany agent staje si˛e agentem martwym 0. Zmiana stanów agenta opisana jest graf przej´sc´ pokazany na rys. 2.2. a. b. 0 ←− a.0 + b.0 −→ 0 Rysunek 2.2: Graf przej´sc´ dla przykładu 2.2. K. Balicki Formalny opis (...) algebry procesów XCCS.

(18) 19. 2.4. Przykłady modeli w j˛ezyku CCS. Przykład 2.3. a.0|b.0 Agent a.0|b.0 przy stanie poczatkowym ˛ moz˙ e wykonać akcj˛e a lub ko-akcj˛e b. Je´sli wykonana najpierw akcje a, to nast˛epnie wykonuje akcj˛e b i staje si˛e agentem martwym 0|0. Je´sli wykonana najpierw akcj˛e b, to nast˛epnie wykonuje akcj˛e a i staje si˛e agentem martwym 0|0. Zmiana stanów agenta opisana jest graf przej´sc´ pokazany na rys. 2.3. a.0|b.0 a. b a.0|0. 0|b.0 a. b 0|0. Rysunek 2.3: Graf przej´sc´ dla przykładu 2.3. Przykład 2.4. a.0|a.0 Agent a.0|a.0 przy stanie poczatkowym ˛ moz˙ e wykonać akcj˛e a lub ko-akcj˛e a lub synchronizacj˛e τ . Je´sli wykonana najpierw akcje a, to nast˛epnie wykonuje akcj˛e a i staje si˛e agentem martwym 0|0. Je´sli wykonana najpierw akcj˛e a, to nast˛epnie wykonuje akcj˛e a i staje si˛e agentem martwym 0|0. Je´sli wykonana najpierw synchronizacj˛e τ , czyli jednoczesne wykonanie akcji komplementarnych a i a, to od razu staje si˛e agentem martwym 0|0. Zmiana stanów agenta opisana jest graf przej´sc´ pokazany na rys. 2.4. a.0|a.0 a. a τ {a, a}. 0|a.0. a.0|0 a. a 0|0. Rysunek 2.4: Graf przej´sc´ dla przykładu 2.4. Przykład 2.5. (a.0|a.0)\{a} Agent (a.0|a.0)\{a} przy stanie poczatkowym ˛ moz˙ e wykonać tylko synchronizacj˛e τ , czyli jednoczesne wykonanie akcji komplementarnych a i a, bo operator restrykcji \ z argumentem {a} zabrania pojedynczego wykonania akcji a i ko-akcji a. Innymi słowy, akcje te sa˛ niewidoczne. Zmiana stanów agenta opisana jest graf przej´sc´ pokazany na rys. 2.5. K. Balicki Formalny opis (...) algebry procesów XCCS.

(19) 20. 2.4. Przykłady modeli w j˛ezyku CCS. (a.0|a.0)\{a}. τ {a, a}. (0|0)\{a} Rysunek 2.5: Graf przej´sc´ dla przykładu 2.5. Wszystkie przedstawione powyz˙ ej przykłady agentów moga˛ generować jedynie skończone sekwencje akcji. Aby zdefiniować systemy, które wykonuja˛ nieskończone ciagi ˛ akcji musimy wykorzystać stałe agentowe i odwołania rekurencyjne. Przykład 2.6. B = a.b.B + c.d.B Agent B przy stanie poczatkowym ˛ moz˙ e wykonać akcj˛e a lub akcj˛e c. Je´sli wykonana najpierw akcj˛e a, to staje si˛e agentem b.B i nast˛epnie wykonuje akcj˛e b aby stać si˛e ponownie agentem B. Je´sli wykonana najpierw akcj˛e c, to staje si˛e agentem d.B i nast˛epnie wykonuje akcj˛e d aby stać si˛e ponownie agentem B. Graf przej´sc´ dla tego przykładu pokazano na rysunkach 2.6 i 2.7. B. b a. d c. b.B. d.B. Rysunek 2.6: LTS - forma „skompresowana”. a.b.B + c.d.B b. d a. b.B. c d.B. Rysunek 2.7: LTS - forma „rozwini˛eta”. Oba grafy sa˛ izomorficzne i maja˛ identyczne etykietowanie łuków, LTS na rys. 2.6 ma form˛e skompresowana,˛ a LTS na rys. 2.7 ma form˛e rozwini˛eta,˛ przez co jest łatwiejszy do analizy. W obu przypadkach stan poczatkowy ˛ jest okre´slony przez w˛ezeł północny.. K. Balicki Formalny opis (...) algebry procesów XCCS.

(20) 21. 2.4. Przykłady modeli w j˛ezyku CCS. Przykład 2.7. Rozpatrzmy model dwuelementowego bufora kolejkowego: QBuffer = (C1 |C2 )\{m}. ≡. QBuffer = (in.m.C1 |m.out.C2 )\{m}. (2.4a). C1 = in.m.C1. (2.4b). C2 = m.out.C2. (2.4c). Agent QBuffer w stanie poczatkowym ˛ moz˙ e wykonać jedynie akcj˛e in po czym staje si˛e agentem (m.C1 |m.out.C2 )\{m}. Z kolei dla tego agenta jedyna˛ moz˙ liwa˛ do wykonania akcja˛ jest synchronizacja τ mi˛edzy akcjami m i m, która prowadzi do agenta (in.m.C1 |out.C2 )\{m}. Dla tego agenta moz˙ liwe sa˛ do wykonania dwie akcje in lub out. Je´sli agent ten wykona najpierw akcj˛e in to stanie si˛e agentem (m.C1 |out.C2 )\{m} a nast˛epnie wykona jedyna˛ moz˙ liwa˛ akcj˛e out, która prowadzi do rozwaz˙ anego juz˙ wcze´sniej stanu (m.C1 |m.out.C2 )\{m}. Je´sli agent ten wykona najpierw akcj˛e out to stanie si˛e agentem (in.m.C1 |m.out.C2 )\{m} a nast˛epnie wykona jedyna˛ moz˙ liwa˛ akcj˛e in, która prowadzi do stanu poczatkowego. ˛ Zasad˛e działania tego bufora pokazanj na rysunku pogladowym ˛ (zobacz rys. 2.10). Graf przej´sc´ dla tego przykładu pokazano na rysunkach 2.8 i 2.9. (m.C1 |C2 )\{m} in. out τ. QBuffer. (m.C1 |out.C2 )\{m} in. out. (C1 |out.C2 )\{m} Rysunek 2.8: LTS - forma „skompresowana” (m.C1 |m.out.C2 )\{m} in (in.m.C1 |m.out.C2 )\{m}. out τ. out. (m.C1 |out.C2 )\{m} in. (in.m.C1 |out.C2 )\{m} Rysunek 2.9: LTS - forma „rozwini˛eta” Oba grafy sa˛ izomorficzne i maja˛ identyczne etykietowanie łuków, pierwszy LTS ma form˛e skompresowana,˛ a drugi rozwini˛eta.˛ W obu przypadkach stan poczatkowy ˛ jest okre´slony przez w˛ezeł zachodni. Aby łatwiej zrozumieć działanie dwuelementowego bufora cyklicznego w odniesieniu do jego LTS’a na rys. 2.10 pokazano jeszcze schemat pogladowy ˛ ilustrujacy ˛ jego dynamik˛e. K. Balicki Formalny opis (...) algebry procesów XCCS.

(21) 22. 2.4. Przykłady modeli w j˛ezyku CCS. [◦][ ] in. out τ. [ ][ ]. [◦][◦] in. out [ ][◦]. Rysunek 2.10: QBuffor - schemat pogladowy ˛ W dwóch ostatnich przykładach zaprezentowano dwa klasyczne problemy synchronizacyjne: model systemu producent-konsument oraz model czytelników i pisarzy. Definicje skryptów CCS dla tych modeli podano w notacji stosowanej w programie Edinburgh Concurrency Workbench (CWB [37]). Program ten jest popularnym narz˛edziem do modelowania i analizy systemów z wykorzystaniem algebr CCS. Program CWB dost˛epny jest w postaci binarnej dla róz˙ nych systemów operacyjnych (Linux, SunOS, Win32). Istnieje równiez˙ moz˙ liwo´sc´ kompilacji spersonalizowanej wersji ze z´ ródeł. Program umoz˙ liwia m.in.: – definiowanie dynamiki agentów, – 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. agent Producer = produce.’put.Producer; agent Consumer = get.consume.Consumer; agent Buffer = put.Buffer1; agent Buffer1 = put.Buffer2 + ’get.Buffer; agent Buffer2 = ’get.Buffer1; set S = {put, get}; agent System = (Producer | Buffer | Consumer)\S;. Listing 2.1: Model CCS systemu producent-konsument. Na listingu 2.1 przedstawiono model systemu producent-konsument z dwuelementowym buforem. Definicja kaz˙ dego z agentów rozpoczyna si˛e od słowa kluczowego agent. Słowo kluczowe K. Balicki Formalny opis (...) algebry procesów XCCS.

(22) 2.4. Przykłady modeli w j˛ezyku CCS. 23. set słuz˙ y do definiowania zbiorów akcji. Akcje wyj´sciowe, czyli ko-akcje, okre´sla si˛e umieszczajac ˛. przed nazwa˛ akcji znak prim ’. System składa si˛e z dwóch procesów (agenty Producer i Consumer), z których pierwszy w kaz˙ dym cyklu swojej pracy wytwarza (akcja produce) komunikat i umieszcza go (akcja ’put) w buforze (agenty: Buffer, Buffer1, Buffer2), a drugi w kaz˙ dym cyklu pobiera (akcja get) komunikat z bufora i konsumuje (akcja consume) go. W omawianym przykładzie bufor jest dwuelementowy, a liczba komunikatów aktualnie przechowywanych w buforze jest reprezentowana za pomoca˛ warto´sci liczbowej przypisanej do stałej agentowej Buffer – brak tej warto´sci oznacza bufor pusty. Akcje put i get ze zbioru S sa˛ akcjami nieobserwowalnymi i słuz˙ a˛ do synchronizacji odpowiednio producenta i konsumenta z buforem. Graf pochodnych dla rozwaz˙ anego systemu, w postaci tekstowej wygenerowanej z uz˙ yciem programu CWB, znajduje si˛e na listingu 2.2. Dodatkowo, celem zwi˛ekszenia przejrzysto´sci, tekst listingu został przeformatowany, a w˛ezły w grafie zostały ponumerowane. (0). System --- produce ---> (’put.Producer | Buffer | Consumer)\S. (9). (Producer | Buffer2 | Consumer)\S --- tau ---> (Producer | Buffer1 | consume.Consumer)\S --- produce ---> (’put.Producer | Buffer2 | Consumer)\S. (0). (1) (6) (11). (Producer | Buffer | Consumer)\S --- produce ---> (’put.Producer | Buffer | Consumer)\S. (1). (11) (’put.Producer | Buffer2 | Consumer)\S --- tau ---> (’put.Producer | Buffer1 | consume.Consumer)\S (8). (7). (Producer | Buffer2 | consume.Consumer)\S --- consume ---> (Producer | Buffer2 | Consumer)\S. (9). --- produce ---> (’put.Producer | Buffer2 | consume.Consumer)\S (10) (2). (1). (Producer | Buffer1 | Consumer)\S --- tau ---> (Producer | Buffer | consume.Consumer)\S. (3). --- produce ---> (’put.Producer | Buffer1 | Consumer)\S. (4). (’put.Producer | Buffer | Consumer)\S --- tau ---> (Producer | Buffer1 | Consumer)\S. (3). (2). (Producer | Buffer | consume.Consumer)\S --- consume ---> (Producer | Buffer | Consumer)\S. (0). --- produce ---> (’put.Producer | Buffer | consume.Consumer)\S (5) (10) (’put.Producer | Buffer2 | consume.Consumer)\S --- consume ---> (’put.Producer | Buffer2 | Consumer)\S (4). (6). (11). (’put.Producer | Buffer1 | Consumer)\S --- tau ---> (Producer | Buffer2 | Consumer)\S. (9). --- tau ---> (’put.Producer | Buffer | consume.Consumer)\S. (5). (Producer | Buffer1 | consume.Consumer)\S --- consume ---> (Producer | Buffer1 | Consumer)\S. (2). --- produce ---> (’put.Producer | Buffer1 | consume.Consumer)\S (7) (5). (’put.Producer | Buffer | consume.Consumer)\S --- tau ---> (Producer | Buffer1 | consume.Consumer)\S. K. Balicki Formalny opis (...) algebry procesów XCCS. (6).

(23) 2.4. Przykłady modeli w j˛ezyku CCS. --- consume ---> (’put.Producer | Buffer | Consumer)\S (7). 24. (1). (’put.Producer | Buffer1 | consume.Consumer)\S --- tau ---> (Producer | Buffer2 | consume.Consumer)\S. (8). --- consume ---> (’put.Producer | Buffer1 | Consumer)\S. (4). Listing 2.2: Graf pochodnych dla systemu producent-konsument. agent Reader1 = ’in.read.out.Reader1; agent Reader2 = ’in.read.out.Reader2; agent Reader3 = ’in.read.out.Reader3; agent Writer1 = ’lock.write.unlock.Writer1; agent Writer2 = ’lock.write.unlock.Writer2; agent Reading = in.In1; agent In1 = ’out.Library + in.In2; agent In2 = ’out.In1 + in.In3; agent In3 = ’out.In2; agent Writing = lock.’unlock.Library; agent Library = Reading + Writing; set S = {in, out, lock, unlock}; agent RW1 = (Library | Reader1 | Reader2 | Reader3 | Writer1 | Writer2)\S;. Listing 2.3: Model CCS systemu czytelnicy i pisarze. Na listingu 2.3 przedstawiono model czytelników i pisarzy. W modelu tym wyst˛epuja˛ dwa typy procesów, które odpowiednio odczytuja˛ i zapisuja˛ dane do współdzielonej zmiennej okre´slanej w modelu mianem czytelni. Czytelnicy moga˛ realizować odczyt równolegle, za´s w przypadku pisarzy wymagany jest dost˛ep do czytelni na wyłaczno´ ˛ sc´ . W prezentowanym modelu uz˙ yto trzech czytelników (agenty: Reader1, Reader2, Reader3) i dwóch pisarzy (agenty: Writer1, Writer2). Na funkcjonowanie kaz˙ dego z czytelników składaja˛ si˛e trzy akcje: wej´scie do czytelni (akcja ’in), odczytanie danych (akcja read) i wyj´scie z czytelni (akcja out). Akcje realizowane przez pisarzy to: zablokowanie dost˛epu do czytelni (akcja lock), zapis danych (akcja write) i odblokowanie dost˛epu do czytelni (akcja ’unlock). Wzajemne wykluczanie czytelników i pisarzy zostało zrealizowane przy pomocy operatora wyboru +, który wzajemnie wyklucza proces odczytu (agent Reading) i proces zapisu (agent Writing). Akcje in, out, lock, unlock ze zbioru S sa˛ akcjami nieobserwowalnymi i słuz˙ a˛ do synchronizacji odpowiednio: dwie pierwsze czytelników z czytelnia˛ a dwie ostatnie pisarzy z czytelK. Balicki Formalny opis (...) algebry procesów XCCS.

(24) 2.5. Podsumowanie. 25. nia.˛ Dla tego modelu pomini˛eto graf przej´sc´ ze wzgl˛edu na stosunkowo duz˙ a˛ liczb˛e w˛ezłów i łuków w tym grafie.. 2.5. Podsumowanie Przedstawiony w niniejszym rozdziale rachunek CCS jest jedna˛ z najbardziej popularnych algebr procesów. Modelowany system moz˙ e być opisany na róz˙ nych poziomach uszczegółowienia, mi˛edzy specyfikacja˛ wymagań a końcowa˛ implementacja.˛ Na podstawie relacji bisymulacji [5], [35] dowodzona jest równowaz˙ no´sc´ poszczególnych modeli, z punktu widzenia obserwowalnych z zewnatrz ˛ akcji. Pozwala to iteracyjne rozwijać opracowany model. Podstawowe ograniczenie zwia˛ zane z opisana˛ algebra˛ procesów dotyczy rozmiaru opisywanego problemu. W przypadku systemów składajacych ˛ si˛e juz˙ z kilkunastu agentów, pojawia si˛e problem zwiazany ˛ z poprawnym opisem komunikacji wewn˛etrznej mi˛edzy agentami. Problem ten nasila si˛e zwłaszcza wtedy, gdy chcemy w jednym systemie umie´scić kilka kopii tego samego agenta. Dotyczy on konieczno´sci wyeliminowania niechcianych połacze´ ˛ n, czy tez˙ odpowiedniego przeetykietowania portów tak, aby funkcjonowała oczekiwana komunikacja. Przedstawiony w rozdziale 3 j˛ezyk XCCS powstał mi˛edzy innymi w celu wyeliminowania tego problemu. W połaczeniu ˛ z koncepcja˛ tagów omówiona˛ w rozdziale 4 rozwiazanie ˛ wydaje si˛e kompletne.. K. Balicki Formalny opis (...) algebry procesów XCCS.

(25) 3. Algebra XCCS. Problemy, które pojawiaja˛ si˛e przy tworzeniu systemów współbiez˙ nych w algebrze CCS łatwo opisać na przykładzie konkatenacji modeli. Typowe post˛epowanie w projektowaniu oprogramowania jak i równiez˙ przy tworzeniu systemów współbiez˙ nych to wykorzystanie istniejacego ˛ juz˙ kodu i modeli. Załóz˙ my, z˙ e mamy przygotowane trzy skrypty CCS i chcemy je razem połaczy´ ˛ c, aby uzyskać nowy model systemu. Bardzo cz˛esto napotykamy nast˛epujace ˛ problemy: 1. Skrypty CCS moga˛ zawierać stałe agentowe o tych samych nazwach. 2. Skrypty CCS moga˛ zawierać akcje wzajemnie do siebie komplementarne, co bardzo cz˛esto okre´sla niepoz˙ adane ˛ synchronizacje pomi˛edzy agentami w złoz˙ onym systemie. 3. Okre´slenie poz˙ adanych ˛ i wyeliminowanie niepoz˙ adanych ˛ synchronizacji pomi˛edzy dwoma skryptami CCS moz˙ e spowodować wystapienie ˛ niechcianych synchronizacji z trzecim skryptem CCS. Wspomniane problemy udało si˛e wyeliminować w j˛ezyku XCCS (eXtended CCS [8], [7], [33], [48]), który jest graficznym rozszerzeniem algebry procesów CCS. Wprowadzenie warstwy graficznej miało ułatwić konstruowanie modeli i zminimalizować popełnianie bł˛edów. W j˛ezyku XCCS przyj˛eto załoz˙ enie, z˙ e wszystkie moz˙ liwe synchronizacje b˛eda˛ okre´slane w sposób jawny w warstwie graficznej.. 3.1. Charakterystyka j˛ezyka XCSS Podstawowa róz˙ nica mi˛edzy algebra˛ CCS i jej rozszerzeniem XCCS dotyczy wspomnianej warstwy graficznej. W j˛ezyku XCCS operatory złoz˙ enia, obci˛ecia i przeetykietowana zostały przeniesione do warstwy graficznej. Agent reprezentowany jest jako owal z nazwa˛ w s´rodku. Porty wejsćiowe agenta reprezentuja˛ okr˛egi, a wyj´sciowe kwadraty, które sa˛ umieszczane na kraw˛edziach owali. Z kaz˙ dym portem skojarzona jest jego etykieta. Obci˛ecie portu reprezentowane jest poprzez zaczernienie odpowiedniego okr˛egu lub kwadratu. Połaczenia ˛ mi˛edzy agentami sa˛ definiowane jawnie i reprezentowane poprzez linie łacz ˛ ace ˛ porty. Połaczenie ˛ musi być definiowane mi˛edzy portem wyj´sciowym i wej´sciowym. Nie ma znaczenia jakie sa˛ etykiety łaczonych ˛ portów. Warunkiem wystapienia ˛ połaczenia ˛ w modelu XCCS jest jego obecno´sc´ w warstwie graficznej, a nie zgodno´sc´ etykiet. Bez jego jawnej definicji nie funkcjonuje ono nawet mi˛edzy portami komplementarnymi o 26.

(26) 3.2. Formalna definicja algebry procesów CSS. 27. identycznych etykietach. Przeniesienie cz˛esći operatorów do warstwy graficznej skutkuje ponadto znacznym uproszczeniem stosowanych równań algebraicznych. W warstwie tej stosowane sa˛ wyłacznie ˛ operatory prefiksu i alternatywy (dla modeli nieczasowych).. Rysunek 3.1: Konstruowanie modeli XCCS w edytorze Inez Na rysunku 3.1 zamieszczono zrzut ekranu prototypowego s´rodowiska Inez zaimplementowanego do konstruowania modeli z j˛ezyku XCCS. Widoczna warstwa graficzna zawiera połaczenie ˛ trzech kopii agenta A, mi˛edzy którymi zdefiniowano dwa połaczenia. ˛ W przeciwieństwie do j˛ezyka CCS w XCCS nie ma tutaj konieczno´sci jawnego reetykietowania portów, aby wskazane połaczenia ˛ ´ funkcjonowały. Srodowisko Inez pozwala równiez˙ na automatyczna˛ konwersj˛e modelu do j˛ezyka CCS w formacie zgodnym z CWB ([37]), w którym to narz˛edziu moz˙ na dokonać formalnej weryfikacji zaprojektowanego modelu. Zaimplementowana konwersja realizuje automatyczne reetykietowanie nazw portów tak, aby w skrypcie CCS funkcjonowały tylko połaczenia ˛ zdefiniowane w warstwie graficznej j˛ezyka XCCS.. 3.2. Formalna definicja algebry procesów CSS W j˛ezyku XCCS w opisie modelu w warstwie tekstowej korzysta si˛e tylko z operatora nast˛epstwa . (kropka), operatora wyboru + oraz nawiasów okragłych, ˛ a dla wersji j˛ezyka z czasem równiez˙ z operatora silnego wyboru + + i opó´znienia $. Na potrzeby formalnego opisu algebry XCCS, zdefiniujemy najpierw podzbiór algebry CCS o nazwie CSS (Calculus of Sequential Systems), w którym zachowamy tylko operatory niezb˛edne w warstwie tekstowej XCCS. Przyjmiemy nast˛epujace ˛ oznaczenia: K. Balicki Formalny opis (...) algebry procesów XCCS.

(27) 28. 3.2. Formalna definicja algebry procesów CSS. – A jest zbiorem nazw, gdzie a, b, . . . ∈ A. – A jest zbiorem ko-nazw (nazw komplementarnych), gdzie a, b, . . . ∈ A. – L := A ∪ A jest zbiorem etykiet, gdzie l, l0 , . . . ∈ L. – Act := L ∪ {τ } jest zbiorem akcji, gdzie α, β, . . . ∈ Act. – K jest zbiorem stałych agentowych, gdzie A, B, C, . . . ∈ K. – E jest zbiorem wyraz˙ eń agentowych okre´slonych przez nast˛epujac ˛ a˛ notacj˛e BNF: E ::= 0 | A | (E) | α.E | E + E. (3.1). gdzie priorytet operatorów jest okre´slony w porzadku ˛ malejacym. ˛ Dodatkowo zakładamy, z˙ e dla kaz˙ dej stałej agentowej A istnieje dokładnie jedno równanie dedef. finiujace ˛ postaci A = E, gdzie E jest wyraz˙ eniem zdefiniowanym przez (3.1), a symbol 0 nie jest zdefiniowany przez z˙ adne równanie. Zbiór reguł przej´sc´ , który okre´sla semantyk˛e operacyjna˛ dla algebry CSS jest podzbiorem zbioru reguł przej´sc´ dla algebry CCS i zawiera nast˛epujace ˛ reguły: Pref. (3.2a). α. α.E → E α. Sum1. E → E0. (3.2b). α. E + F → E0 α. Sum2. F → F0. (3.2c). α. E + F → F0 α. Con1. E → E0 α. A → E0. def. (A = E). (3.2d). α. Con2. E → E0 α. E→A. def. (A = E 0 ). (3.2e). α. Brac. E → E0 α. (E) → E 0. (E ≡ E1 + E2 ). (3.2f). Symbol CSS b˛edzie oznaczał nie tylko zredukowana˛ algebr˛e procesów CCS, ale równiez˙ zbiór tychz˙ e algebr. Aby unikna´ ˛c nieporozumień zbiór CSS zredukowanych algebr procesów b˛edziemy zapisywali pochylona˛ czcionka.˛ Podobnie jak w przypadku algebry CCS, algebry CSS b˛edziemy def. definiowali przy pomocy ciagu ˛ równań algebraicznych postaci A = E. Nazwa stałej agentowej w pierwszym równaniu algebraicznym ciagu ˛ równań b˛edzie równiez˙ oznaczać nazw˛e całego ciagu ˛ CSS i . Dla wygody, ciag ˛ CSS i ∈ CSS nazywać b˛edziemy skryptem lub algebra˛ lub programem lub modelem CSS. Przyjmiemy nast˛epujace ˛ oznaczenia: K. Balicki Formalny opis (...) algebry procesów XCCS.

(28) 3.3. Wprowadzenie do algebry procesów XCCS. 29. – A(CSS i ) jest zbiorem wszystkich akcji algebry CSS i – A(CSS i ) jest zbiorem wszystkich ko-akcji algebry CSS i – K(CSS i ) jest zbiorem wszystkich stałych agentowych algebry CSS i. 3.3. Wprowadzenie do algebry procesów XCCS Praktyka modelowania realnych systemów współbiez˙ nych z wykorzystanie algebry procesów CCS pokazała, z˙ e wi˛ekszo´sc´ z nich moz˙ na przedstawić w postaci złoz˙ enia równoległego fragmentów systemu, które zachowuja˛ si˛e w sposób sekwencyjny. Z tego wzgl˛edu w pierwszej fazie prac nad algebra˛ procesów XCCS zdecydowali´smy si˛e rozwaz˙ ać graficzne rozszerzenia dla standardowych form współbiez˙ nych – patrz definicja 4.1 w rozdziale 4. Na wst˛epie podamy dwa przykłady, które ułatwia˛ zrozumienie formalnej definicji graficznego rozszerzenia algebry procesów XCCS. Rozpatrzmy model dwu-elementowego bufora kolejkowego w postaci algebry CCS. Queue = (B1 |B2 )\{pass} A = in.out.A. (3.3a) (3.3b). B1 = A[pass/out]. (3.3c). B2 = A[pass/in]. (3.3d). Zanim przedstawimy analogiczny model w postaci algebry XCCS podamy najpierw krótki opis własno´sci diagramów XCCS: a) bloczki reprezentuja˛ składowe systemu, które zachowuja˛ si˛e w sposób sekwencyjny; b) bloczki maja˛ okre´slone nazwy, które pozwalaja˛ je zidentyfikować; c) bloczki maja˛ przypisane algebry CSS, które definiuja˛ ich zachowanie; d) bloczki maja˛ interfejs czyli etykietowane porty wej´sciowe i wyj´sciowe; e) etykiety portów okre´slaja˛ akcje i ko-akcje upowaz˙ nione do synchronizacji; f) bloczki moga˛ si˛e komunikować z otoczeniem przez widoczne porty izolowane; g) bloczki nie moga˛ si˛e komunikować z otoczeniem przez niewidoczne porty izolowane; h) bloczki moga˛ si˛e komunikować przez połaczone ˛ ze soba˛ porty komplementarne. Rozróz˙ niamy dwa rodzaje algebr procesów albo inaczej diagramów XCCS: płaskie i pełne. W diagramach płaskich w algebrach przypisanych do bloczków nie uz˙ ywamy ko-akcji. W skrypcie CCS równowaz˙ nym diagramowi płaskiemu akcje odpowiadajace ˛ etykietom portów wyj´sciowych zostana˛ zamienione na ko-akcje. K. Balicki Formalny opis (...) algebry procesów XCCS.

(29) 30. 3.3. Wprowadzenie do algebry procesów XCCS. B1. B2 A. in. pass. out. A in. A = in.out.A; out. Rysunek 3.2: Diagram XCCS dwu-elementowego bufora kolejkowego Skrypt CCS z przykładu 3.3 odpowiada w sposób równowaz˙ ny diagramowi XCCS z rys. 3.2. Powyz˙ szy diagram składa si˛e z dwóch bloczków B1 oraz B2 komunikujacych ˛ si˛e ze soba.˛ Oba te bloczki maja˛ przypisana˛ algebr˛e A. Interfejs bloczka B1 jest okre´slony przez izolowany widoczny port wej´sciowy B1 .in i niewidoczny port wyj´sciowy B1 .out. Interfejs bloczka B2 jest okre´slony przez niewidoczny port wej´sciowy B2 .in i izolowany widoczny port wyj´sciowy B2 .out. Porty B1 .out i B2 .in zostały ze soba˛ połaczone, ˛ a zatem moga˛ si˛e ze soba˛ komunikować. Etykieta pass na linii łacz ˛ acej ˛ porty komplementarne nie jest cz˛esćia˛ definicji diagramu, ale pozwala wygenerować równowaz˙ ny skrypt CCS identyczny ze skryptem na podstawie którego został utworzy diagram. W algorytmach konwersji diagramów XCCS do algebr CCS nie ma potrzeby stosowania w wynikowym skrypcie CCS operatora reetykietowania. Zatem skrypt CCS równowaz˙ ny do diagramu z rys. 3.2 i wygenerowany w sposób automatyczny moz˙ e mieć postać: Queue = (B1 |B2 )\{pass}. (3.4a). B1 = in.pass.B1. (3.4b). B2 = pass.out.B2. (3.4c). J˛ezyk modelowania XCCS moz˙ na traktować jako narz˛edzie wspomagajace ˛ tworzenie modeli w algebrze CCS (diagramy pomagaja˛ nam tworzyć poprawne skrypty CCS) lub jako samodzielny formalizm matematyczny niekoniecznie sći´sle zwiazany ˛ z algebra˛ CCS. Rozpatrzmy teraz przykład pełnego diagramu XCCS z rys. 3.3. B1. B2 A. a. c. b. b. A = a.'b.A;. B. B = b.'c.B;. Rysunek 3.3: Pełny diagram XCCS Diagram składa si˛e z dwóch bloczków B1 oraz B2 komunikujacych ˛ si˛e mi˛edzy soba.˛ Interfejs bloczka B1 jest okre´slony przez izolowany widoczny port wej´sciowy B1 .a dost˛epny na zewnatrz ˛ systemu oraz niewidoczny port wyj´sciowy B1 .b przeznaczony do komunikacji wewnatrz ˛ systemu. Interfejs bloczka B2 jest okre´slony przez izolowany widoczny port wyj´sciowy B2 .c dost˛epny na zewnatrz ˛ systemu oraz niewidoczny port wej´sciowy B2 .b przeznaczony do komunikacji wewnatrz ˛ systemu. Zachowanie bloczka B1 jest okre´slone przez skrypt A, a zachowanie bloczka B2 jest okres´lone przez skrypt B. Skrypt A cyklicznie wykonuje akcj˛e a, a po niej ko-akcj˛e b. Skrypt B cykliczK. Balicki Formalny opis (...) algebry procesów XCCS.

(30) 31. 3.3. Wprowadzenie do algebry procesów XCCS. nie wykonuje akcj˛e b, a po niej ko-akcj˛e c. Nazwa a jest etykieta˛ widocznego portu wej´sciowego B1 .a, a zatem wykonanie akcji a moz˙ na interpretować jako komunikacj˛e s´rodowiska z bloczkiem B1 . Nazwa c jest etykieta˛ widocznego portu wyj´sciowego B2 .c, a zatem wykonanie ko-akcji c moz˙ na interpretować jako komunikacj˛e bloczka B2 ze s´rodowiskiem. Nazwa b jest etykieta˛ niewidocznego portu wyj´sciowego B1 .b, a zatem ko-akcja b bloczka B1 jest niewidoczna i nie moz˙ e wykonać si˛e samodzielnie. Analogicznie, nazwa b jest etykieta˛ niewidocznego portu wej´sciowego B2 .b, a zatem akcja b bloczka B2 jest niewidoczna i nie moz˙ e wykonać si˛e samodzielnie. Port wyj´sciowy B1 .b jest połaczony ˛ z portem wej´sciowym B2 .b, a zatem ko-akcja b i akcja b moga˛ ze soba˛ synchronizować, czyli wykonać si˛e jednocze´snie. Synchronizacj˛e pomi˛edzy ko-akcja˛ b i akcja˛ b moz˙ na interpretować jako komunikacj˛e bloczka B1 z bloczkiem B2 . Zachowanie opisanego powyz˙ ej modelu odpowiada zachowaniu agenta Q1 . Q1 = (B1 |B2 )\{b}. (3.5a). B1 = a.b.B1. (3.5b). B2 = b.c.B2. (3.5c). Zwróćmy uwag˛e, z˙ e powyz˙ szy skrypt jest w pewien sposób podobny do skryptu dla modelu bufora. Łatwo tez˙ zauwaz˙ yć, z˙ e diagram z rys. 3.3 moz˙ na w sposób trywialny przetłumaczyć na równowaz˙ ny skrypt CCS. Trywialny algorytm konwersji diagramów XCCS do algebr procesów CCS moz˙ na scharakteryzować w sposób nast˛epujacy. ˛ 1. Wynikowy skrypt CCS jest złoz˙ eniem równoległym algebr przypisanych do bloczków. 2. Algebry przypisane do bloczków przyjmuja˛ nazwy tych bloczków. 3. W zbiorze restrykcji umieszczamy etykiety niewidocznych portów. Zwróćmy uwag˛e, z˙ e trywialny algorytm konwersji b˛edzie poprawny tylko dla bardzo niewielkiej liczby diagramów XCCS. Grafy przej´sc´ , które opisuja˛ zachowanie powyz˙ szego skryptu CCS przedstawiono na rys. 3.4 i 3.5. Oba grafy sa˛ izomorficzne, LTS u góry ma form˛e skompresowana,˛ a LTS u dołu jest łatwiejszy do analizy. W obu przypadkach stan poczatkowy ˛ jest okre´slony przez „w˛ezeł zachodni”. (b.B1 |B2 )\{b} c. a Q1. τ c. (b.B1 |c.B2 )\{b} a. (B1 |c.B2 )\{b} Rysunek 3.4: LTS dla algebry Q1 - forma „skompresowana”. K. Balicki Formalny opis (...) algebry procesów XCCS.

(31) 32. 3.4. Formalna definicja algebry procesów XCCS. (b.B1 |b.c.B2 )\{b} a (a.b.B1 |b.c.B2 )\{b}. c τ. c. (b.B1 |c.B2 )\{b} a. (a.b.B1 |c.B2 )\{b} Rysunek 3.5: LTS dla algebry Q1 - forma „rozwini˛eta”. 3.4. Formalna definicja algebry procesów XCCS Definicja 3.1. Algebra˛ procesów XCCS nazywamy krotk˛e XCCS = (B , CA, CSS , CR, in, out, ϑ, ρ). (3.6). spełniajac ˛ a˛ nast˛epujace ˛ warunki: (i) B jest zbiorem bloczków (ang. agent blocks). (ii) CA jest zbiorem akcji komunikacyjnych (ang. communication actions). (iii) CSS jest zbiorem algebr procesów CSS i (CSS). Uwaga: B˛edziemy równiez˙ rozwaz˙ ać podzbiór j˛ezyka modelowania XCCS , który nazywamy płaskim (ang. plain) XCCS , gdzie dla kaz˙ dego CSS i zbiór ko-akcji spełnia warunek A(CSS i ) = ∅. (iv) CR ⊆ OutP ×InP jest relacja˛ opisujac ˛ a˛ komunikacj˛e mi˛edzy bloczkami (ang. communication relation), gdzie: InP = {(Bi , a) : Bi ∈ B ∧ a ∈ in(Bi )}. (3.7). jest zbiorem portów wej´sciowych, a OutP = {(Bi , a) : Bi ∈ B ∧ a ∈ out(Bi )}. (3.8). jest zbiorem portów wyj´sciowych. Dodatkowo definiujemy: – P = InP ∪ OutP jest zbiorem wszystkich portów. – b : P → B jest funkcja,˛ która kaz˙ demu portowi przypisuje bloczek, z którym zwiazany ˛ jest dany port, gdzie: b(Bi , a) = Bi dla (Bi , a) ∈ InP b(Bi , a) = Bi dla (Bi , a) ∈ OutP K. Balicki Formalny opis (...) algebry procesów XCCS. (3.9) (3.10).

(32) 33. 3.4. Formalna definicja algebry procesów XCCS. – ca : P → CA jest funkcja,˛ która kaz˙ demu portowi przypisuje jego akcj˛e komunikacyjna,˛ która˛ nazywamy etykieta˛ portu (ang. port label), gdzie: ca(Bi , a) = a dla (Bi , a) ∈ InP. (3.11). ca(Bi , a) = a dla (Bi , a) ∈ OutP. (3.12). Relacja CR musi spełniać nast˛epujace ˛ warunki: ∀pout1 , pout2 ∈ OutP. ∀pin1 , pin2 ∈ InP :. pout1 ∼ pin1 ∧ pout2 ∼ pin1 ∧ pout2 ∼ pin2 ⇒ pout1 ∼ pin2 ,. (3.13). ∀(pout1 , pin1 ), (pout2 , pin2 ) ∈ CR : pout1 = pout2 ⇒ (pin1 6= pin2 ⇒ b(pin1 ) 6= b(pin2 )) i pin1 = pin2 ⇒ (pout1 6= pout2 ⇒ b(pout1 ) 6= b(pout2 )),. (3.14). ∀(pout, pin) ∈ CR : b(pout) 6= b(pin) ∧ v(pout) = v(pin).. (3.15). (v) in : B → 2CA jest funkcja,˛ która kaz˙ demu bloczkowi przypisuje zbiór jego wej´sciowych akcji komunikacyjnych. (vi) out : B → 2CA jest funkcja,˛ która kaz˙ demu bloczkowi przypisuje zbiór jego wyj´sciowych akcji komunikacyjnych. Je´sli rozwaz˙ amy płaski j˛ezyk modelowania XCCS , to dodatkowo funkcje in i out musza˛ spełniać nast˛epujacy ˛ warunek ∀Bi ∈ B : in(Bi ) ∩ out(Bi ) = ∅.. (3.16). (vii) ϑ : P → {v, i} jest funkcja,˛ która dla kaz˙ dego portu komunikacyjnego okre´sla, czy jest on widoczny (ang. visible) czy niewidoczny (ang. invisible). (viii) ρ : B → CSS jest funkcja,˛ która kaz˙ demu bloczkowi Bi ∈ B przypisuje zredukowana˛ algebr˛e procesów CSS i ∈ CSS . Motywacje i wyja´snienia (i) + (iii) Bloczki reprezentuja˛ fragmenty systemu, które wykonuja˛ si˛e w sposób sekwencyjny. Zachowanie bloczków okre´slone jest przez przypisane do nich algebry CSS i . Rozróz˙ niamy dwa rodzaje j˛ezyka modelowania XCCS z diagramami płaskimi i pełnymi. W płaskim j˛ezyku modelowania XCCS w algebrach CSS przypisanych do bloczków nie wyst˛epuja˛ ko-akcje. Wi˛ekszo´sc´ rzeczywistych modeli systemów współbiez˙ nych da si˛e wyrazić za pomoca˛ diagramów płaskich. Pełne diagramy XCCS rozpatrujemy ze wzgl˛edu na zachowanie zgodno´sci z algebra˛ CCS, a ponadto pozwalaja˛ one na okre´slenie tzw. dwukierunkowej komunikacji, a co za tym idzie uproszczenie struktury diagramu. Przykład komunikacji dwukierunkowej podany jest w rozdziale 4.3 przy opisie problemu jedzacych ˛ filozofów. Je´sli w tek´scie nie zaznaczono inaczej K. Balicki Formalny opis (...) algebry procesów XCCS.

(33) 34. 3.4. Formalna definicja algebry procesów XCCS. lub nie wynika to z kontekstu, to domy´slnie przyjmujemy, z˙ e rozpatrywany przez nas diagram XCCS jest płaski. (ii) + (iv) + (v) + (vi) Kaz˙ dy bloczek ma okre´slony interfejs czyli zbiór wej´sciowych i wyj´sciowych portów przez które moz˙ e si˛e komunikować z innymi bloczkami lub otoczeniem. Nazwy czyli inaczej etykiety portów wej´sciowych i wyj´sciowych okre´slone sa˛ przez funkcje odpowiednio in i out. Relacja CR musi spełniać warunek „niesymetrycznej” trój-przechodnio´sci (3.13). Je´sli porty połaczone ˛ sa˛ w taki sposób, z˙ e tworza˛ drog˛e, to w obr˛ebie tej drogi kaz˙ da para portów komplementarnych musi być ze soba˛ połaczona. ˛ Rozwaz˙ my przykład z rys. 3.6. Porty połaczone ˛ linia˛ ciagł ˛ a˛ tworza˛ drog˛e, a zatem na diagramie musi tez˙ pojawić si˛e połaczenie ˛ zaznaczone linia˛ przerywana.˛ A. B A. b. D. A = a.b.A; B = c.d.B; C = e.f.C; D = g.h.D;. B. d. C D. C h. f. Rysunek 3.6: Warunek niesymetrycznej trój-przechodnio´sci A. B A. a. B. A = a.b.A; B = c.d.B;. B. A = a.b.A; B = c.d.B;. c b. a) A. B A. c a d. b). Rysunek 3.7: Przykłady niepoprawnych połacze´ ˛ n Warunek (3.14) mówi, z˙ e je´sli dowolny port połaczony ˛ jest z wi˛ecej niz˙ jednym portem komplementarnym, to kaz˙ dy z tych portów komplementarnych musi znajdować si˛e na innym bloczku. Diagramy pokazane na rys. 3.7 sa˛ zatem niepoprawne. Warunek (3.15) mówi, z˙ e nie wolno łaczy´ ˛ c ze soba˛ portów które, które znajduja˛ na jednym bloczku. Przykład takiego niepoprawnego połaczenie ˛ jest widoczny na rys. 3.8 a). K. Balicki Formalny opis (...) algebry procesów XCCS.

(34) 35. 3.5. Relacja synchronizacji. Porty widoczne moz˙ na łaczy´ ˛ c tylko z widocznymi, a porty niewidoczne moz˙ na łaczy´ ˛ c tylko z niewidocznymi. Kolejny przykład niepoprawnych połacze´ ˛ n pokazany jest na rys. 3.8 b). A A = a.b.A;. A. a b. a) A. B A. B b. A = a.b.A; B = a.b.B;. b. b). Rysunek 3.8: Inne przykłady niepoprawnych połacze´ ˛ n Warunek (3.16) mówi, z˙ e je´sli rozwaz˙ amy płaskie diagramy XCCS, to wej´sciowe i wyj´sciowe porty komunikacyjne danego bloczka musza˛ mieć róz˙ ne nazwy. Płaski diagram z niepoprawnymi etykietami portów widoczny jest na rys. 3.9. B A = a.b.A;. A. a a. Rysunek 3.9: Płaski diagram XCCS z niepoprawnymi etykietami portów. 3.5. Relacja synchronizacji Niech b˛edzie dana algebra procesów XCCS. Dla relacji komunikacji CR i dla dowolnego portu p ∈ P definiujemy: CR(p) = {x ∈ P : (x, p) ∈ CR ∨ (p, x) ∈ CR}. (3.17). Je´sli p ∈ OutP , to zbiór CR(p) zawiera wszystkie porty wej´sciowe, z którymi połaczony ˛ jest port p. Je´sli p ∈ InP , to zbiór CR(p) zawiera wszystkie porty wyj´sciowe, z którymi połaczony ˛ jest port p. Okre´slamy odwzorowanie SR : P → 2P : ( {p} je´sli CR(p) = ∅ SR(p) = S CR(p) ∪ x∈CR(p) CR(x) je´sli CR(p) = 6 ∅. (3.18). Spełnione sa˛ warunki: ∀p1 , p2 ∈ P : SR(p1 ) = SR(p2 ) ∨ SR(p1 ) ∩ SR(p2 ) = ∅, S. p∈P. SR(p) = P.. K. Balicki Formalny opis (...) algebry procesów XCCS. (3.19) (3.20).

(35) 36. 3.6. Definicje pomocnicze. Zatem odwzorowanie SR wyznacza podział zbioru P . Relacj˛e synchronizacji SR ⊆ P × P definiujemy w nast˛epujacy ˛ sposób: def. (p1 , p2 ) ∈ SR ⇐⇒ SR(p1 ) = SR(p2 ).. (3.21). [p]SR = SR(p),. (3.22). ∀p1 , p2 ∈ P : b(p1 ) = b(p2 ) ⇒ (ca(p1 ) 6= ca(p2 ) ⇒ [p1 ] ∩ [p2 ] = ∅).. (3.23). Spełnione sa˛ warunki:. Klasy abstrakcji relacji SR okre´slone przez porty nalez˙ ace ˛ do tego samego bloczka sa˛ parami rozłaczne. ˛ Relacja SR jest relacja˛ równowaz˙ no´sci, która wyznacza podział zbioru portów P na klasy abstrakcji. Je´sli klasa abstrakcji zawiera tylko jeden port, to jest on izolowany i nie komunikuje si˛e z z˙ adnym innym portem. Je´sli klasa abstrakcji zawiera wi˛ecej niz˙ jeden port, to kaz˙ da para portów komplementarnych w tej klasie komunikuje si˛e ze soba.˛. 3.6. Definicje pomocnicze W tym rozdziale podamy definicje pomocnicze, oraz zaproponujemy pewne konwencje, które pozwalaja˛ upro´scić terminologi˛e stosowana˛ w odniesieniu do j˛ezyka modelowania XCCS. Definicja 3.2. Zapis v.p oraz i.p oznacza odpowiednio widoczny oraz niewidoczny port p ∈ P , czyli: def. v.p = p def. i.p = p. gdzie ϑ(p) = v. (3.24). gdzie ϑ(p) = i. (3.25). Definiujemy zbiory wszystkich portów widocznych V i niewidocznych I: V = {p ∈ P : ϑ(p) = v}. (3.26). I = {p ∈ P : ϑ(p) = i}. (3.27). Definicja 3.3. Mówimy, z˙ e port p ∈ P jest izolowany, je´sli CR(p) = ∅.. (3.28). Definiujemy zbiór wszystkich portów izolowanych: Iso = {p ∈ P : CR(p) = ∅}. (3.29). Widoczne porty izolowane okre´slaja˛ interfejs dla danego diagramu XCCS. Poprzez te porty diagram moz˙ e komunikować si˛e z otoczeniem. W planowanej wersji hierarchicznej j˛ezyka modelowania XCCS diagram zostanie zastapiony ˛ bloczkiem hierarchicznym wokół którego znajda˛ si˛e wła´snie widoczne porty izolowane, które okre´sla˛ dla niego interfejs komunikacyjny. K. Balicki Formalny opis (...) algebry procesów XCCS.