Ph.D. In Computer Engineering

CE 608 | Course Introduction and Application Information

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

#	Content	PC Sub	* Contribution Level
#	Content	PC Sub	1	2	3	4	5
1	will be able to express the behavior of systems using specification formalisms such as process algebras at different level of abstraction.
2	will be able to explain the basic principles underlying various notions of behavioral equivalences.
3	will be able to describe computational properties of systems using modal logic.
4	will be able to use verification tools to demonstrate whether design models satisfy their desired properties.
5	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

WEEKLY SUBJECTS AND RELATED PREPARATION STUDIES

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

EVALUATION SYSTEM

Semester Activities	Number	Weighting	LO 1	LO 2	LO 3	LO 4	LO 5
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

ECTS / WORKLOAD TABLE

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

COURSE LEARNING OUTCOMES AND PROGRAM QUALIFICATIONS RELATIONSHIP

#	PC Sub	Program Competencies/Outcomes	* Contribution Level
#	PC Sub	Program Competencies/Outcomes	1	2	3	4	5
1	Understands and applies the foundational theories of Computer Engineering in a high level.		-	-	-	-	X
2	Possesses a great depth and breadth of knowledge about Computer Engineering including the latest developments.		-	-	-	X	-
3	Can reach the latest information in Computer Engineering and possesses a high level of proficiency in the methods and abilities necessary to comprehend it and conduct research with it.		-	-	X	-	-
4	Conducts a comprehensive study that introduces innovation to science and technology, develops a new scientific procedure or a technological product/process, or applies a known method in a new field.		-	-	-	X	-
5	Independently understands, designs, implements and concludes a unique research process in addition to managing it.		-	-	-	-	X
6	Contributes to science and technology literature by publishing the output of his/her academic studies in respectable academic outlets.		-	-	-	X	-
7	Interprets scientific, technological, social and cultural developments and relates them to the general public with a commitment to scientific objectivity and ethical responsibility.		-	-	-	X	-
8	Performs critical analysis, synthesis and evaluation of ideas and developments in Computer Engineering.		-	-	-	-	X
9	Performs verbal and written communications with professionals as well as broader scientific and social communities in Computer Engineering, by using English at least at the European Language Portfolio C1 General level, performs written, oral and visual communications and discussions in a high level.		-	-	X	-	-
10	Develops strategies, policies and plans about systems and topics that Computer Engineering uses, and interprets the outcomes.		-	-	-	X	-