Specification and Verification of Real Systems | Facultatea de Informatică Iaşi

Logica Temporală a Acţiunilor

Numele cursului

Logica Temporală a Acţiunilor

Cod

CS4104O1

Generaţia	Informatică zi, 2004 - 2008					Pachet	7
Nivel de studii	Licenţă	An	4	Semestru	1	Statut	Opţional

Titularul disciplinei	Titlu academic şi ştiinţific
	Profesor, Dr., Cristian Masalagiu

Discipline absolvite anterior

Obiective	Însuşirea conceptelor de bază pentru a putea specifica şi verifica sistemele reale cu un mare risc în funcţionare, cu ajutorul logicii (neclasice). Învăţarea unui limbaj concret/implementat comercial de specificare şi verificare (TLA+).
Tematica generală	Logica cu predicate de ordinul I. Logica temporală (LTL, CTL, etc.). Verificarea programelor (totală, parţială; clasic şi modern). Model checking. Arbori, limbaje infinite. Alte modele pentru specificarea şi verificarea „corectitudinii comportărilor” unui sistem real. Statistică, complexitate.
Tematica seminariilor / laboratoarelor	Tematica 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 predare	Se 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

C.D. Masalagiu – Utilizarea metodelor formale în specificarea şi verificarea sistemelor concurente, Editura MATRIX-ROM, Bucureşti, 2005 (in Romanian).
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, Université de Liège, 2000).
L. Lamport – Specifying Systems: The TLA+ Language and Tools for Software and Hardware Engineers, Addison-Wesley, U. S. A., 2002.
INTERNET sites (they will become precise during the semester).

Evaluare	condiţii	Prezenţa la toate laboratoarele este obligatorie.
	criterii	Examină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.
	forme	La 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 finale	Nota 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.