Verificare formală

Curs, anul VI, sem. I 2002/2003
Cadru didactic: Marius Minea
marius@cs.utt.ro

Informații despre curs

Curs: Miercuri, 10-12, ASPC sala CC
Proiect: Marti, 18:10-20, B528 (săptămâni pare)
Consultații: Joi 12-14 sau la cerere (e-mail)

Evaluare:
Activitate pe parcurs (proiecte și teme): 50%
Examen parțial: 25%
Examen final: 25%

Proiecte și teme

Proiect 1
Modelarea și verificarea unui protocol de comunicație folosind Spin.
Distribuit: 8 octombrie. Termen de predare: 6 noiembrie.
Proiect 2
Modelarea și verificarea unui protocol de coerență în SMV.
Distribuit: 5 noiembrie. Termen de predare: 10 decembrie.

Material prezentat la curs

  1. Metode formale. Introducere (PDF 98kB, sau 6 folii/pagină)
  2. Model checking. Algoritmi de bază (PDF 100kB, sau 6 folii/pagină)
  3. Model checking cu automate. Metode cu ordonare parțială. (PDF 245kB, sau 6 folii/pagină)
  4. Model checking simbolic. Diagrame de decizie binare (PDF 440kB, sau 6 folii/pagină)
  5. Echivalențe și preordini. Raționament compozițional. (PDF 207kB, sau 6 folii/pagină)
  6. Metode de abstracție (PDF 114kB, sau 6 folii/pagină)
  7. Elemente de logică matematică (PDF 80kB, sau 6 folii/pagină)
  8. Verificarea sistemelor în timp discret și continuu (PDF 102kB, sau 6 folii/pagină)
  9. Analiza și verificarea programelor (PDF 80kB, sau 8 folii/pagină)
  10. Verificarea protocoalelor de securitate (PDF 75kB, sau 8 folii/pagină)

Material prezentat in orele de proiect

  1. Spin. Câteva exemple.
    Verificatorul, interfața grafică Xspin, și exemple: pentru Unix (.tar.gz 302kB) și Windows 95/98/NT (.zip 283kB)
    Un pachet opțional pentru vizualizarea automatelor.
    Cartea lui Gerard Holzmann, Design and Validation of Computer Protocols
  2. SMV. Câteva mici exemple. Manualul (PS 484kB).
    Verificatorul NuSMV e instalat pe bigfoot in /usr/local/nusmv-2.0.2/bin/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 si clasificare concisă, cu multe exemple de aplicație.

Model checking

E. Clarke, O. Grumberg, D. Long. "Verification Tools for Finite State Concurrent Systems", A Decade of Concurrency -- Reflections and Perspectives, REX School/Symposium, Noordwijkerhout, Netherlands. Lecture Notes in Computer Science, vol. 803, pp. 124-175, Springer Verlag, iun. 1993. (PS, 736kB)
Un excelent articol de sinteză. Conține majoritatea materiei predate la primele cursuri.

Metode cu ordonare parțială

E. M. Clarke, O. Grumberg, M. Minea, D. Peled. "State space reduction using partial order techniques", International Journal on Software Tools for Technology Transfer", vol. 2, no. 3, pp. 279-287, Springer Verlag, 1999 (PDF, 182kB)
O introducere cu un minim de formalism.

Diagrame de decizie binare

R. E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation", IEEE Transactions on Computers, vol. C-35 no. 8, pp. 677--691, aug. 1986. (PS, 384kB)
Articolul clasic care a introdus BDD-urile.

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

E. Clarke, O. Grumberg, D. Long. "Model checking", Proceedings of the International Summer School on Deductive Program Design Marktobedorf, Germany, 1994. In M. Broy, "Deductive Program Design", NATO ASI Series F vol. 152, Springer Verlag, 1996. (PS, 438 kB)
Majoritatea materiei predate la cursurile 5 și 6.

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ă.

Ultima actualizare: 14 ianuarie 2003.

marius@cs.utt.ro