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 1
Modelarea și verificarea unui protocol de comunicație folosind Spin.
Distribuit: 7 octombrie. Termen de predare: 28 octombrie.

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

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.

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 cursul 4 și 5.

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


Marius Minea
Last modified: Wed Feb 4 18:10:09 EET 2004