GRADUATE SCHOOL
M.SC. in Computer Engineering (With Thesis)
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 | 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 | ||||
*1 Lowest, 2 Low, 3 Average, 4 High, 5 Highest