CE 608 | Course Introduction and Application Information - M.SC. in Computer Engineering (With Thesis)

Course Name

Formal Specification and Verification of Concurrent Systems

Code	Semester	Theory (hour/week)	Application/Lab (hour/week)	Local Credits	ECTS
CE 608	Fall/Spring	3	0	3	7.5

Prerequisites	None
Course Language	English
Course Type	Elective
Course Level	Third Cycle
Mode of Delivery	-
Teaching Methods and Techniques of the Course	-
National Occupation Classification	-
Course Coordinator	-
Course Lecturer(s)	Yrd. Doç. Dr. Ufuk ÇELİKKAN
Assistant(s)	-

Course Objectives

The goal of this course is an in depth study of formalisms used to reason about and verify reactive systems to determine if a system meet its specification in a precise manner. These specification formalisms include process algebra based languages such as CCS and CSP which also have logical characterizations. Formal methods have been successfully used in industrial applications such circuit equivalence checking and protocol verification. Protocol verification will be discussed as an application area of formal methods. A verification tool will be used to create formal specifications of systems and verify them.

Learning Outcomes

The students who succeeded in this course;

will be able to express the behavior of systems using specification formalisms such as process algebras at different level of abstraction.
will be able to explain the basic principles underlying various notions of behavioral equivalences.
will be able to describe computational properties of systems using modal logic.
will be able to use verification tools to demonstrate whether design models satisfy their desired properties.
will be able to choose most useful formal techniques and tools when faced with a real-world verification problem.

Course Description

This course is on overview of specification formalisms and techniques used to reason about concurrent and reactive systems.

Course Category	Core Courses
	Major Area Courses	X
	Supportive Courses
	Media and Management Skills Courses
	Transferable Skill Courses

Week	Subjects	Related Preparation	Learning Outcome
1	Introduction to formal specification, verification and correctness. What do we mean by "formal" methods? What are they for and why are they used? Formal verification vs. testing.	Lecturer slides
2	Formal Specification Languages and Tools	Aceto et.al. “Reactive Systems: Modelling Specification and Verification”
3	LOTOS : Language of Temporal Ordering specifications.	T Bolognesi, E Brinksma. "Introduction to the ISO specification language LOTOS" Computer Networks and ISDN systems, 1987.
4	Labelled transition systems. Communicating processes	Hoare. “Communicating Sequential Processes” Ch. 1.
5	Process Algebra Language CSP (Communicating Sequential Processes)	Hoare. “Communicating Sequential Processes” Ch. 2-3.
6	Process Algebra Language CCS (Calculus of Communicating Systems)	Robin Milner, “Communication and Concurrency” Ch. 1-3
7	Introduction to equivalences. Equivalence based verification with CCS	Robin Milner, “Communication and Concurrency” Ch. 4.
8	Equivalence based verification with CCS (continued)	Robin Milner, “Communication and Concurrency” Ch. 4.
9	Midterm
10	Preorder based verification with CCS	Cleaveland and Steffen "A preorder for partial process specifications"LNCS, 1990, Vol 458, 141-151.
11	Logical Characterization of CCS: Hennessy-Milner Logic	Robin Milner, “Communication and Concurrency”, Ch 10.
12	Counters, Buffers, Alternating bit protocol, Meaningful examples	Specification and Verification” pages 50 - 53
13	Paper presentations
14	Paper presentations
15	Review
16	-

Course Notes/Textbooks	Instructor material.
Suggested Readings/Materials	1) Luca Aceto, Anna Ingolfsdottir, Kim Larsen and Jiri Srba “Reactive Systems: Modelling Specification and Verification”, Cambridge University Press, 2007 2.) Robin Milner, “Communication and Concurrency”, (3rd ed.). Prentice Hall. 1989.3) C. A. R. Hoare. “Communicating Sequential Processes”, Prentice Hall,1985

Semester Activities	Number	Weigthing
Participation
Laboratory / Application
Field Work
Quizzes / Studio Critiques
Portfolio
Homework / Assignments
Presentation / Jury	1	20
Project	1	20
Seminar / Workshop
Oral Exams
Midterm	1	25
Final Exam	1	35
Total

Weighting of Semester Activities on the Final Grade	3	65
Weighting of End-of-Semester Activities on the Final Grade	1	35
Total

Semester Activities	Number	Duration (Hours)	Workload
Theoretical Course Hours (Including exam week: 16 x total hours)	16	3	48
Laboratory / Application Hours (Including exam week: '.16.' x total hours)	16		0
Study Hours Out of Class	15	4	60
Field Work			0
Quizzes / Studio Critiques			0
Portfolio			0
Homework / Assignments			0
Presentation / Jury	1	30	30
Project	1	30	30
Seminar / Workshop			0
Oral Exam			0
Midterms	1	20	20
Final Exam	1	37	37
		Total	225

#	PC Sub	Program Competencies/Outcomes	* Contribution Level
#	PC Sub	Program Competencies/Outcomes	1	2	3	4	5
1	Accesses information in breadth and depth by conducting scientific research in Computer Engineering; evaluates, interprets and applies information.		-	-	-	-	X
2	Is well-informed about contemporary techniques and methods used in Computer Engineering and their limitations.		-	-	-	X	-
3	Uses scientific methods to complete and apply information from uncertain, limited or incomplete data; can combine and use information from different disciplines.		-	-	X	-	-
4	Is informed about new and upcoming applications in the field and learns them whenever necessary.		-	-	-	X	-
5	Defines and formulates problems related to Computer Engineering, develops methods to solve them and uses progressive methods in solutions.		-	-	-	X	-
6	Develops novel and/or original methods, designs complex systems or processes and develops progressive/alternative solutions in designs		-	-	-	X	-
7	Designs and implements studies based on theory, experiments and modelling; analyses and resolves the complex problems that arise in this process.		-	-	X	-	-
8	Can work effectively in interdisciplinary teams as well as teams of the same discipline, can lead such teams and can develop approaches for resolving complex situations; can work independently and takes responsibility.		-	X	-	-	-
9	Engages in written and oral communication at least in Level B2 of the European Language Portfolio Global Scale.		-	-	X	-	-
10	Communicates the process and the results of his/her studies in national and international venues systematically, clearly and in written or oral form.		-	X	-	-	-
11	Is knowledgeable about the social, environmental, health, security and law implications of Computer Engineering applications, knows their project management and business applications, and is aware of their limitations in Computer Engineering applications.		X	-	-	-	-
12	Highly regards scientific and ethical values in data collection, interpretation, communication and in every professional activity.		-	X	-	-	-

CE 608 | Course Introduction and Application Information

WEEKLY SUBJECTS AND RELATED PREPARATION STUDIES

EVALUATION SYSTEM

ECTS / WORKLOAD TABLE

COURSE LEARNING OUTCOMES AND PROGRAM QUALIFICATIONS RELATIONSHIP

NEW GÜZELBAHÇE CAMPUS

GLOBAL CAREER

CONTRIBUTION TO SCIENCE

VALUING PEOPLE

BENEFIT TO SOCIETY