Verificare formală

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

Informaţii despre curs

Curs: Marţi, 18-20, A303
Proiect: Marţi, 20-21, B528 A+B
Consultaţii: la cerere (e-mail)

Evaluare:
Activitate pe parcurs (proiecte şi teme): 50%
Examen parţial: 25 noiembrie 2003 (25%)
Examen final: 25%: 7 februarie 2004, ora 9, A110
Situatia curenta

Proiecte şi teme

Proiect 2
Modelarea unui protocol de coerenta de memorie folosind SMV.
Distribuit: 28 octombrie. Termen de predare: 25 noiembrie.

Proiect 3
Modelarea şi verificarea unui sistem de fabricatie folosind UPAAAL.
Distribuit: 2 decembrie. Termen de predare: 18 ianuarie.

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, PS, 1:1 şi PDF, 1:6 pentru listat
4. Model checking cu automate. Relaţii între modele. Raţionament compoziţional PDF, 1:1, PS, 1:1 şi PDF, 1:6 pentru listat
5. Reducerea spaţiului stărilorPDF, 1:1, PS, 1:1 şi PDF, 1:6 pentru listat
6. Elemente de logică matematică PDF, 1:1 şi PDF, 1:6 pentru listat
7. Verificarea sistemelor în timp real PDF, 1:1 şi PDF, 1:6 pentru listat
8. Verificarea programelor PDF, 1:1 şi PDF, 1:6 pentru listat
9. Verificarea programelor în practică PDF, 1:1 şi PDF, 1:6 pentru listat
10. Analiza programelor PDF, 1:1 şi PDF, 1:6 pentru listat
11. Verificarea protocoalelor de securitate PDF, 1:1 şi PDF, 1:6 pentru listat

Nişte notiţe incomplete pentru prima parte a cursului.

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
2. SMV. Câteva mici exemple. Manualul (PS 484kB).
   Verificatorul NuSMV

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.

Model checking

Diagrame de decizie binare

R. E. Bryant. "Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification", International Conference on Computer Design, pp. 236--243, nov. 1995 (PS, 240kB)
Un articol de sinteză despre BDD-uri şi variantele lor.

Relaţii între structuri, raţionament compoziţional şi abstracţie

H. Peng, S. Tahar. "A Survey on Compositional Verification", Technical Report, Concordia University, Canada, Department of Electrical and Computer Engineering, dec. 1998. (PS, 475 kB)
O prezentare introductivă, elementară.