GRADUATE SCHOOL
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 | - | |||||
| Course Coordinator | - | |||||
| Course Lecturer(s) | ||||||
| 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;
|
| Course Description | This course is on overview of specification formalisms and techniques used to reason about concurrent and reactive systems. |
|
|
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 |
| 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 | 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 |
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
|
#
|
Program Competencies/Outcomes |
* Contribution Level
|
||||
|
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 | ||||
*1 Lowest, 2 Low, 3 Average, 4 High, 5 Highest