Obiective
- Însusirea conceptelor de baza pentru a putea specifica si verifica sistemele reale cu un mare risc în functionare, cu ajutorul logicilor neclasice.
- Învatarea unui limbaj concret de specificare si verificare (TLA+).
Tematica generală:
- Logica cu predicate de ordinul I.
- Logica temporală (LTL, CTL, etc.).
- Verificarea programelor (totală, parţială; clasic şi modern).
- Arbori, limbaje infinite.
- Model checking.
- Alte modele pentru specificarea şi verificarea "corectitudinii comportarilor" unui sistem real, sisteme concurente formale, sisteme tranzitionale, diagrame de decizie binare.
Tematică
Tematica va fi fixata de coordonator la prima întâlnire. Ea va cuprinde exemplificări ale cursurilor deja predate,
teme imediate, pentru acasă şi proiecte de durată mai îndelungată. Se vor folosi metodele clasice (Expunerea sistematică a cunostintelor,
Conversaţia, Problematizarea şi învăţarea prin descoperire, Modelarea, etc.). Cursurile vor fi predate utilizând video.
Laboratoarele vor fi axate pe învăţarea unui limbaj comercial existent (TLA+).
Cursuri anterioare necesare
- Cursul de Logica, anul I.
- Opţional, Cursul de Programare logică din anul II.
Bibliografie
- C.D. Masalagiu, V. Alaiba - Utilizarea metodelor formale în specificarea si verificarea sistemelor concurente, Editura MATRIX-ROM, Bucuresti, 2007 (va apare).
- M. Huth, M. Ryan - Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, England, 2000, ISBN 0-521-65200-6.
- P. Wolper - The Algorithmic Verification of Reactive Systems (course notes, Universite de Liege, 2000).
- L. Lamport - Specifying Systems: The TLA+ Language and Tools for Software and Hardware Engineers, Addison-Wesley, U. S. A., 2002.
- Site-uri INTERNET care vor fi precizate.
- E. M. Clarke, Bernd-Holger Schlingloff, Model Checking, Handbook of Automated Reasoning, 2001
- Slide-uri TLA
Modalităţi de evaluare (cerinţe):
- Prezenţa la toate laboratoarele este obligatorie.
- Examinarile pe parcurs de la laborator genereaza maxim 90 puncte, iar examenul final 30 puncte.
Dacă se obţin sub 40 puncte inclusiv, cursul nu este promovat.
- Punctajul ar putea fi îmbunătăţit prin rezolvarea unor probleme suplimentare sau susţinerea unor lucrări de verificare neanunţate (aceste activităţi vor fi desfăşurate în cadrul Cursului).
- Descrierea modalităţii de evaluare la laborator se găseşte pe pagina laboratorului.
- Nu se promovează fără nici un punct obţinut la Curs (la examen sau prin teme/teste pe parcurs).
- Se va face o clasificare finală de "tip Gauss", conform regulamentelor în vigoare.
|
