Verificare formală

Curs, anul VI, sem. I 2004/2005 (versiune anterioară: 2003/2004)
Cadru didactic: Marius Minea
marius@cs.upt.ro

Informaţii despre curs

Curs: marţi 18-20, A314
Orele din săptămâna 2 se recuperează în săptămâna 3.
Proiect: marţi 20-21 şi joi 8-9, B528 A+B
Consultaţii: la cerere (e-mail)

Evaluare: Situatia curenta
Activitate pe parcurs (proiecte şi teme): 50%.
Examen parţial: 25%
Examen final: 25%

Proiecte şi teme

Proiect 2
Modelarea şi verificarea unui sistem de fabricaţie folosind UPPAAL.
Distribuit: 9 noiembrie. Termen de predare: 7 decembrie.

Material prezentat la curs

1. Metode formale. Introducere PDF, 1:1 si 1:6, pentru listat
2. Model checking. Noţiuni de bază PDF, 1:1 si 1:6, pentru listat
3. Model checking simbolic. Diagrame de decizie binare PDF, 1:1 si 1:6, pentru listat
4. Model checking cu automate. Relatii intre modele. Rationament compozitional PDF, 1:1 si 1:6, pentru listat
5. Verificarea sistemelor în timp real PDF, 1:1 si 1:6, pentru listat
6. Elemente de logică matematică PDF, 1:1 si 1:6, pentru listat
7. Abstracţie. Metode de reducere a spaţiului stărilor PDF, 1:1 si 1:6, pentru listat
8. Verificarea programelor PDF, 1:1 si 1:6, pentru listat
9. Analiza fluxului de date PDF, 1:1 si 1:6, pentru listat
10. Verificarea protocoalelor de securitate PDF, 1:1 si 1:6, pentru listat
11. Interpretare abstractă PDF, 1:1 si 1:6, pentru listat
    şi un set de folii de curs de Doug Gregor, Rensellaer Polytechnic (RPI)
12. Verificarea programelor în practică PDF, 1:1 si 1:6, pentru listat

Material prezentat in orele de proiect

1. Verificatorul Spin.
   Un exemplu simplu şi un manual pentru limbajul de modelare PROMELA.
   Verificatorul, interfaţa grafică Xspin, şi exemple: pentru Unix (.tar.gz) şi Windows (.zip)
   Cartea lui Gerard Holzmann, Design and Validation of Computer Protocols

Bibliografie

Articole introductive

E. M. Clarke, R. P. Kurshan. "Computer Aided Verification", IEEE Spectrum, vol. 33, no. 6, pp. 61-67, iun. 1996. (PS, 6.1MB)
Un istoric al verificării formale in hardware, cu o descriere detaliată a mai multor aplicaţii.

E. M. Clarke, J. M. Wing. "Formal Methods. State of the Art and Future Directions", ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, dec. 1996. (PS, 188kB)
O definitie şi clasificare concisă, cu multe exemple de aplicaţie.