Laborator SVI-SW
Aspecte administrative
- credit disciplina: 5 pct.
- nota = 40% (curs) + 60% (laborator)
- predarea temei 1 se face sub forma printata a unui document structurat in 3 sectiuni (antet cu
nume si email student + prezentare tema; listing promela; min. 3 conditii temporale verificate);
intarzierea predarii temei este penalizata cu 1 pct/saptamana; este incurajata propunerea subiectului temei 1 de catre studenti, cu conditia sa fie validata de
catre indrumatorul laboratorului(de ex. subiectul poate fi din aria de cercetare sau a lucrarii
de dizertatie);
- predarea temei 2 se va face in sesiune;
Lucrari de laborator
- Introducere in PROMELA. Simularea in SPIN (prima parte , a 2-a parte)
- Validare + Enuntarea temei 1.
- Logica Temporala Liniara + Activitate aferenta temei 1.
- Aplicatii (facultativ)- modelarea si validarea protocolului cu chei publice Needham-Schroeder + Predarea temei 1
- Translatarea formulelor LTL in automate Buchi generalizate + Enuntarea temei 2
- Determinizarea automatelor GBN. Automatul Rabin + Activitate aferenta temei 2
- Activitate aferenta temei 2
Teme de laborator
- 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.
- 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
- [0] Spin homepage
- [1] Translatoare LTL -> automat non-determinist Buchi: LTL2BA, Buchi Sore, GOAL,
LBT
- [2] Translatoare LTL -> automat determinist Rabin/Street: LTL2DSTAR, LTL3DRA
- [3] M.Huth, M.Ryan, "Logic in Computer Science", 2nd ed. Cambridge Univ. Press, 2004
- [4] M.Vardi, "An automata-theoretic approach to LTL"
- [5] Construieste diagrame MSC WebSeqDiagrams, MscGen
- [6] Construieste grafuri cu: GraphViz
- [7] Scapy: generator/receptor de trafic
- [8] picoManual de Scapy
- [9] Beej's tutorial on Berkley Sockets API for C programming
- [10] Despre programare in C/Linux GNU C Library
- [11] H.R. Andersen, "An introduction to Binary Decision Diagrams (BDDs)", 1997
- [12] R.Gerth, D.Peled, M.Vardi,P.Wolper, "Simple on-the-fly automatic verification of LTL", 1995