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