SY (systemy sieciowe i komputerowe)JP (języki programowania i logika)
Opis przedmiotu:
Z procesami współbieżnymi obecnie informatycy muszą radzić sobie nieustannie,
zarówno w środowiskach zwartych (architektury wielordzeniowe), jak i
rozproszonych (np. protokoły sieciowe). Projektowanie i analiza takich
systemów nie jest łatwym zadaniem. Wykorzystanie istniejących narzędzi do
modelowania i badania własności systemów współbieżnych wymaga znajomości
teorii, na których są one oparte, czyli algebr procesów.
Algebry procesów służą do opisywania i badania zachowania systemów
współbieżnych za pomoca środków algebraicznych. "Klasyczne" algebry procesów
to CCS (Calculus of Communicating Systems, R.Milner), CSP (Communicating
Sequential Processes, T.Hoar) i ACP (Algebra of Communicating Processes,
J.A.Bergstra, J.W.Klop).
W trakcie wykładu zostanie przedstawiona algebra mCRL2, będąca rozszerzeniem
ACP o typy danych (w stylu języków programowania funkcyjnego, z funkcjami
wyższego rzędu), czas i multiakcje. Jest ona zaimplementowa w postaci ciągle
rozwijanego pakietu narzędzi mCRL2 (http://www.mcrl2.org/). Będą przedstawione
m.in. etykietowane systemy przejść, bisymulacja, specyfikacja własności
procesów, logika Hennessy’ego-Milnera, μ-rachunek, a także najważniejsze
narzędzia z pakietu mCRL2.
Wymagania:
Metody programowania
Logika dla informatyków
Wskazane zaliczenie programowania fukcyjnego
Literatura:
1\. Baeten J.C.M., Basten T., Reniers M.A., Process Algebra: Equational
Theories of Communicating Processes, Cambridge University Press, Cambridge
2010.
2\. Fokkink W.J., Introduction to Process Algebra (2nd ed.), Springer-Verlag,
Berlin 2007.
3\. Fokkink W.J., Modelling Distributed Systems, Springer-Verlag, Berlin 2007.
4\. Groot J.F., Mousavi M.R., Modeling and Analysis of Communicating Syatema,
MIT Press, Cambridge, Mass. 2014
5\. Sangiorgi D., Introduction to Bisimulation and Coinduction, Cambridge
University Press, Cambridge 2012.
