Przedmiot: Weryfikacja protoko.BŽłŽów komunikacyjnych wspomagana komputerowo


Typ zajŽęŽć: wykŽład 30 godzin + Žćwiczenia 30 godzin + laboratorium 30 godzin


Cel zajŽęŽć: nauczenie doboru wŽłaŽściwej metody weryfikacji i 
odpowiednich narzŽędzi; uczulenie studentŽów na ograniczenia 
obliczeniowe formalnej weryfikacji i wskazanie sposobŽów ich 
przezwyciŽęŽżenia.

SŽłuchacze zdobŽędŽą praktycznŽą znajomoŽśŽć kilku wybranych narzŽędzi
wspomagajŽących proces weryfikacji systemŽów wspŽóŽłbieŽżnych i 
rozproszonych (CWB, SPIN i UPPAAL).
ZapoznajŽą siŽę rŽównieŽż z wynikami teoretycznymi leŽżŽącymi u podstaw
tych narzŽędzi oraz z algorytmami w nich zaimplementowanymi.
Wyniki matematyczne zostanŽą omŽówione tylko w zakresie niezbŽędnym do
dobrego zrozumienia dziaŽłania wspomnianych narzŽędzi i sprawnego z 
nich korzystania. Zostanie rŽównieŽż omŽówiona zŽłoŽżonoŽśŽć obliczeniowa 
niektorych zadaŽń weryfikacyjnych.


Program:

- model matematyczny procesŽów wspŽóŽłbieŽżnych: algebra procesŽów CCS, 
  silna i sŽłaba bisymulacja jako strategia w grze, przeglŽąd rŽównowaŽżnoŽści
  semantycznych dla procesŽów, hierarchia modeli: od automatŽów ze stosem 
  do etykietowanych sieci Petri'ego

- najwaŽżniejsze logiki do opisu wŽłasnoŽści procesŽów wspŽóŽłbieŽżnych: 
  LTL, CTL, rachunek mi

- omŽówienie narzŽędzi: CWB, SPIN, UPPAAL, przykŽłady modelowania i 
  weryfikacji wybranych protokoŽłŽów przy uŽżyciu tych narzŽędzi

- weryfikacja modelowa (ang. model checking): algorytm dla rachunku mi
  oparty na grach i na tableau (CWB), algorytm dla LTL oparty na tableau
  i na automatach Buchi'ego (SPIN), rozstrzygalne fragmenty dla niektŽórych
  klas systemŽów nieskoŽńczeniestanowych
  
- weryfikacja rŽównowaŽżnoŽści bisymulacyjnej: efektywny
  algorytm dla systemŽów skoŽńczeniestanowych, zŽłoŽżonoŽśŽć obliczeniowa
  dla niektŽórych klas systemŽów nieskoŽńczeniestanowych, nierozstrzygalnoŽśŽć
  dla CCS i dla etykietowanych sieci Petri'ego

- automaty z czasem: technika regionŽów, efektywne struktury danych,
  algorytmy weryfikacyjne (UPPAAL)

- metody redukcji rozmiaru przestrzeni stanŽów (SPIN, UPPAAL),
  technika przyŽśpieszania (UPPAAL)


Proponowane podrŽęczniki:

- Handbook of Process Algebra, 
  Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, Editors, 
  rozdziaŽły 1, 4, 6, 9

- Modal and Temporal Properties of Processes,
  Colin Stirling

- Design and Validation of Computer Protocols
  Gerard J. Holzmann

- http://www.dcs.ed.ac.uk/home/cwb/

- http://spinroot.com/spin/whatispin.html

- http://www.docs.uu.se/docs/rtmv/uppaal/


ZajŽęcia wymagane do zaliczenia przed wykŽładem:

Do zrozumienia wykŽładu nie jest konieczna znajomoŽśŽć Žżadnego z
przedmiot.AŽów, natomiast przydatny mo.BŽże siŽę okazaŽć wczeŽśniejszy kontakt 
z nastŽępujŽącymi przedmiotami: 
- programowanie wspŽóŽłbieŽżne, 
- semantyka i weryfikacja, 
- jŽęzyki, automaty i obliczenia.


Uwagi:

Zaliczanie przedmiotu: samodzielny projekt praktyczny wykonany
przy uŽżyciu jednego z poznanych narzŽędzi. Dla chŽętnych: egzamin
pisemny obejmujŽący treŽśŽć wykŽładu.

Ograniczenie na liczbŽę uczestnikŽów: 30