Formalny opis wizualnej algebry procesów XCCS
mgr Krzysztof Balicki
Promotor: dr hab. Marcin Szpyrka, prof. nadzw. AGH
Dyscyplina: Informatyka

W rozprawie w sposób formalny zdefiniowany wizualną algebrę procesów XCCS (ang. eXtended Calculus of Concurent Systems). Modele wyrażone w algebrze XCCS mają postać diagramów, które składają się z dwóch warstw: graficznej i tekstowej. Warstwa graficzna reprezentuje sekwencyjne składowe systemu współbieżnego i możliwe interakcje między nimi. Natomiast warstwa tekstowa dostarcza opisu zachowania dla sekwencyjnych składowych systemu. Dla modeli opisanych z wykorzystaniem algebry XCCS można dokonać formalnej analizy z zastosowaniem metod i narzędzi właściwych dla algebr CCS lub metod bazujących na analizie etykietowanych systemów przejść (LTS).

Język XCCS można potraktować w dwojaki sposób jako:

1. Formalizm usprawniający tworzenie poprawnych skryptów w algebrze CCS,
2. Niezależny język modelowania współbieżnego bazujący na algebrze CCS.

Mając na uwadze pierwsze z zastosowań w pracy opisano algorytm konwersji diagramów XCCS do algebr CCS. Algorytm ten dokonuje automatycznego re-etykietowania nazw akcji w taki sposób, aby w wynikowych skrypcie CCS pojawiły się tylko te synchronizacje, które zostały określone w warstwie graficznej na diagramie XCCS. Na potrzeby algorytmu konwersji dla diagramów XCCS opracowano formalne definicje dla tzw. konfliktów i zaciemnień. Konflikty wskazują etykiety portów składowych sekwencyjnych, które muszą zostać poddane re-etykietowaniu, aby wyeliminować niepożądane synchronizacje w wynikowych skrypcie CCS. Zaciemniania wskazują natomiast etykiety portów składowych sekwencyjnych, które muszą zostać poddane re-etykietowaniu, aby w wynikowym skrypcie CCS nie pojawiły akcje niewykonywalne, które na diagramie XCCS są wykonywalne.

Mając na uwadze drugie z zastosowań w pracy zdefiniowano rozszerzenie algebry CCS o koncepcję tagów. Koncepcja ta rozszerza algebrę CCS o nowy mechanizm synchronizujący, który nie wymaga re-etykietowania nazw akcji. Koncepcja tagów w prosty sposób eliminuje problem z przestrzenią nazw akcji w algebrze CCS, co jest szczególnie istotne w przypadku, gdy tworzymy modele systemów na bazie opracowanych wcześniej modułów. Skrypty CCS z mechanizmem tagów w sposób ściśle równoważny reprezentują diagramy XCCS co pozwala na generowania grafów przejść i analizę diagramów XCCS przy pomocy klasycznych metod znanych z algebr procesów. Analiza diagramów XCCS jest również możliwa poprzez generowanie „równoważnych” im skryptów CCS, ale wymaga to zaimplementowania mechanizmu sprzężenia zwrotnego, gdyż wynikowe skrypty CCS mogą zawierać re-etykietowane nazwy akcji. Warto podkreślić, że algorytm konwersji diagramów XCCS do skryptów CCS z tagami, który podano w rozprawie, jest znacznie prostszy od algorytmu opisanego poprzednio. Koncepcja tagów została również wykorzystana do semi-graficznej symulacji diagramów XCCS i jest znacznie bardziej czytelna niż ma to miejsce w przypadku czysto tekstowej symulacji znanej z narzędzi właściwych dla algebr CCS (CWB).

Alternatywna metodą weryfikacji własności modeli z języku XCCS jest wykorzystanie technik weryfikacji modelowej i pakietu CADP. W tym celu dla modelu generowany jest etykietowany system przejść (graf LTS), a oczekiwane własności są specyfikowane z użyciem logiki modalnej μ. Weryfikacja spełnialności formuł jest w tym przypadku realizowana z użyciem pakietu CADP.

Ponadto, diagramy XCCS rozszerzono o mechanizm hermetyzacji znany z obiektowych języków programowania. Udział w synchronizacji mogą brać tylko te akcje składowych sekwencyjnych diagramu, które odpowiadają etykietom portów komunikacyjnych. Pozostałe akcje są wewnętrzne i nie mogą synchronizować.

1. Balicki K., Szpyrka M.: Formal Definition of XCCS Modelling Language. Fundamenta Informaticae 93 (2009) 1-15
2. Balicki K., Szpyrka M.: Tag Abstraction for XCCS Modeling Language. In: Proc. of the CS&P’2009 Workshop, vol. 1, pp. 26-37, Warsaw University 2009
3. Szpyrka M., Balicki K.: XCCS - graphical extension of CCS language. In: Proc. of Mixdes 2006, the 14th International Conference Mixed Design of Integrated Circuits and Systems, Ciechocinek, Poland (2007) 688-693
4. Balicki K.: The Traffic Lights Control System Modelled with the Use of Coloured Petri Nets with Time. In: Proc. of the CS&P’2004 Workshop, pp. 1-11, Humboldt-Universitat zu Berlin 2004
5. Szpyrka M., Matyasik P., Mrówka R., Witalec W., Baniewicz J., Balicki K.: Introduction to Alvis modelling language. Pomiary Automatyka Kontrola, vol. 57, nr 9 (2011) 1086-1089