SY (systemy sieciowe i komputerowe)JP (języki programowania i logika)
Opis przedmiotu:
Z procesami wspołbieżnymi obecnie informatycy muszą radzić sobie nieustannie,
zarowno w środowiskach zwartych (architektury wielordzeniowe), jak i
rozproszonych (np. protokoły sieciowe). Projektowanie i analiza takich
systemow nie jest łatwym zadaniem. Wykorzystanie istniejących narzędzi do
modelowania i badania własności systemow wspołbieżnych wymaga znajomości
teorii, na ktorych są one oparte, czyli algebr procesow.
Algebry procesow służą do opisywania i badania zachowania systemow
wspołbieżnych za pomoca środkow algebraicznych. "Klasyczne" algebry procesow
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ęzykow 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
procesow, logika Hennessy'ego-Milnera, μ-rachunek, a także najważniejsze
narzędzia z pakietu mCRL2.
Wymagania:
Programowanie
Logika dla informatykow
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\. Sangiorgi D., Introduction to Bisimulation and Coinduction, Cambridge
University Press, Cambridge 2012.
Czwartki godz.12:00-12:45 (konieczne jest wcześniejsze uzgodnienie). Możliwe są też inne terminy po uzgodnieniu za pośrednictwem poczty elektronicznej: zs@cs.uni.wroc.pl.
