Universitatea A. I. Cuza Iaşi


Logica Temporală a Acţiunilor

Numele cursuluiLogica Temporală a Acţiunilor CodCS4104O1
Generaţia Informatică zi, 2004 - 2008 Pachet 7
Nivel de studii Licenţă An 4 Semestru 1 Statut Opţional
Nr. de ore pe săptămânăNr. total de ore pe semestruNr. de ore de lucru individualCrediteMod de evaluareLimba de predare
CSLPr
2 2 0 0 56 0 6 E ro
Titularul disciplineiTitlu academic şi ştiinţific
Profesor, Dr., Cristian Masalagiu
Discipline absolvite anterior
Obiective
  1. Însuşirea conceptelor de bază pentru a putea specifica şi verifica sistemele reale cu un mare risc în funcţionare, cu ajutorul logicii (neclasice).
  2. Învăţarea unui limbaj concret/implementat comercial de specificare şi verificare (TLA+).
Tematica generală
  1. Logica cu predicate de ordinul I.
  2. Logica temporală (LTL, CTL, etc.).
  3. Verificarea programelor (totală, parţială; clasic şi modern).
  4. Model checking.
  5. Arbori, limbaje infinite.
  6. Alte modele pentru specificarea şi verificarea „corectitudinii comportărilor” unui sistem real.
  7. Statistică, complexitate.
Tematica seminariilor / laboratoarelorTematica laboratoarelor va fi fixată de coordonator la prima întâlnire, conform tematicii precizate. Oricum, ea va cuprinde exemplificări ale cursurilor deja predate, teme „imediate, pentru acasă” şi proiecte de durată mai îndelungată.
Metode de predareSe vor folosi metodele clasice (Expunerea sistematică a cunoştinţelor, Conversaţia, Problematizarea şi învăţarea prin descoperire, Modelarea, etc.). Cursurile vor fi predate utilizând videoproiectorul. Laboratoarele vor fi axate pe învăţarea limbajului co
Bibliografie
  1. C.D. Masalagiu – Utilizarea metodelor formale în specificarea şi verificarea sistemelor concurente, Editura MATRIX-ROM, Bucureşti, 2005 (in Romanian).
  2. M. Huth, M. Ryan – Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, England, 2000, ISBN 0-521-65200-6.
  3. P. Wolper – The Algorithmic Verification of Reactive Systems (course notes, Université de Liège, 2000).
  4. L. Lamport – Specifying Systems: The TLA+ Language and Tools for Software and Hardware Engineers, Addison-Wesley, U. S. A., 2002.
  5. INTERNET sites (they will become precise during the semester).
EvaluarecondiţiiPrezenţa la toate laboratoarele este obligatorie.
criteriiExaminările pe parcurs de la laborator generează maxim 90 puncte iar examenul final 30 puncte (vor fi 3 subiecte a câte 10 puncte). Condiţia de promovabilitate este de a se obţine minim 50 puncte.
formeLa laborator vor exista 6 teme cotate cu câte 10 puncte (maxim) şi un proiect mai complex, cotat cu 30 puncte (totul va fi preczat în timp util).
formula notei finaleNota finală se obţine prin însumarea punctajului şi împărţirea la 10. Punctajele peste 100 vor genera tot nota 10. Se va face şi o „redistribuire” de tip Gauss, conform regulamentelor în vigoare.

© 2006-2010 FII | despre site | intranet