Specification and Verification of Real Systems

Temporal Logics of Actions

Course name

Temporal Logics of Actions

Code

CS4104O1

Class	Computer Science, 2004 - 2008					Package	7
Level	Undergraduate	Year	4	Semester	1	Status	Optional

Hours per week				Total hours per semester	Total hours of individual work	Credits	Evaluation type	Teaching language
C	S	L	Pr
2	2	0	0	56	0	6	E	ro

Taught by	Academic and scientific title, name
	Professor, PhD, Cristian Masalagiu

Required courses

Objectives	Getting minimal skills for specifying and verifying real “risky” systems, by using non-classical logics (temporal logic being the main concern). Learning a concrete and commercial specification and verification language (the “Temporal Logic of Actions” of L. Lamport – more precisely, TLA+).
General thematics	First-order predicate logic. Modal logic. Temporal logics (LTL, CTL, etc.). Program verification (partial and total). New directions. Model checking.. Trees and infinite languages. Other models for specifying real concurrent systems.
Seminary / Laboratory thematics	The themes will be fixed by the teacher at the beginning of the semester, according to the specified context. They will include the knoledge verification for the previous courses, short examples to be programmed and executed and larger projects.
Teaching methods	All the classical didactic methods will be used: systematic exposure of knoledge, conversation, learning „by descovery”, etc. The Courses will be taught using a retro- or video-porojector. A commercial language (e. g., TLA+) will be taught at the laborat

Bibliography

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

Evaluation	conditions	All the 14-th lab’s have to be confirmed by the presence of the student.
	criterias	The on-line tests during the normal practical activity (laboratory) may generate 90 points (maximum, see below). To “graduate” the course, a minimum of 50 points is need.
	modes	Concerning the “lab”. During the semester activity, there will be 6 themes (each quoted at 10 points, maximum) and a more complex project (quoted at 30 points, maximum).
	formula	The final grade is computed by first summing up all the obtained poins and then by dividing the result by ten. The grades will be then rounded such as to get a Gauss curve for the given year of study (see the regulations). The grades grater than 10 will be rounded to ten.