Rozprawa doktorska zawiera formalny opis algebry procesów XCCS (ang. extended Calculus of Communicating Systems). Modele XCCS 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, a warstwa tekstowa zawiera opis zachowania dla sekwencyjnych składowych systemu. Modele XCCS można formalnie analizować z zastosowaniem metod i narzędzi właściwych dla algebr CCS lub metod bazujących na analizie etykietowanych systemów przejść (grafy LTS). W tym drugim podejściu, dla modelu generowany jest graf LTS, a oczekiwane własności są specyfikowane z użyciem logiki modalnej mu. Weryfikacja spełnialności formuł jest w tym przypadku realizowana z użyciem pakietu CADP.
Język XCCS można potraktować jako formalizm usprawniający tworzenie poprawnych skryptów w algebrze CCS oraz jako niezależny język modelowania współbieżnego bazujący na algebrze CCS.
W odniesieniu do pierwsze go podejścia, w pracy opisano algorytm konwersji diagramów XCCS do algebr CCS. Algorytm ten dokonuje automatycznego re-etykietowania nazw akcji tak, aby w wynikowych skrypcie CCS występowały tylko te synchronizacje, które zostały określone w warstwie graficznej modelu XCCS.
W odniesieniu do drugiego podejścia, w pracy zdefiniowano rozszerzenie algebry CCS o koncepcję tagów, tj. nowy mechanizm synchronizujący, który nie wymaga re-etykietowania nazw akcji.
The PhD thesis contains a formal description of XCCS process calculus (extended Calculus of Communicating Systems). XCCS models are composed of two layers: graphical and textual. The graphical layer represents sequential components of a concurrent system under consideration and interactions between them. The textual layer defines the behaviour of the sequential components. XCCS models can be verified using CCS methods and tools or using labelled transition systems (LTS graphs). In the latter approach, an LTS graph is generated for an XCCS model, the model properties are specified using mu modal logic and the CADP toolbox is used to check whether the properties hold for the considered model.
The XCCS language can be treated both as a formalism for generation correct CCS scripts or as an independent modelling language. For the former approach an algorithm of transformation of an XCCS model into a CCS script has been described in the thesis. The algorithm automatically relabels actions to guarantee that only synchronisations described in the XCCS graphical layer are possible. For the latter approach the so-called tags have been included into XCCS language. Tags are a new synchronisation mechanism that does not use the relabel function.
