Laborator SVI-SW  

Aspecte administrative

Lucrari de laborator

  1. Introducere in PROMELA. Simularea in SPIN (prima parte a 2-a parte)
  2. Validare + Enuntarea temei 1.
  3. Logica Temporala Liniara + Activitate aferenta temei 1.
  4. Aplicatii (facultativ)- modelarea si validarea protocolului cu chei publice Needham-Schroeder + Predarea temei 1
  5. Translatarea formulelor LTL in automate Buchi generalizate + Enuntarea temei 2
  6. Determinizarea automatelor GBN. Automatul Rabin + Activitate aferenta temei 2
  7. Activitate aferenta temei 2

Teme de laborator

  1. Se va specifica formal protocolul [1) cu retransmisie neselectiva fara confirmari negative; 2) cu retransmisie neselectiva cu confirmari negative; 3) cu retransmisie selectiva fara confirmari negative; 4) cu retransmisie selectiva cu confirmari negative; 5) TCP; 6) SIP] si se vor valida proprietatile sale folosind validatorul Spin si limbajul LTL.
  2. Sa se implementeze o procedura in Scapy care sa monitorizeze traficul de retea in timp real cu scopul de a detecta [1) o sesiune HTTP; 2) o sesiune FTP; 3) o sesiune Telnet; 4) o sesiune SSH, 5) o sesiune BitTorrent, etc.]

Referat asociat cursului

Referatul trebuie sa contina: [TBD]
Dimensiunea minima a referatelor este de 4 pagini (2/student).

Referinte