SWE408 Formal Methods in Software Engineering

---

Course Description

Introduction to the use of mathematical models of software systems for their specification and validation, finite state machine models, models of concurrent systems, verification of models, and limitations.

Prerequisites

Software Engineering & Data Structures courses

Course Objectives

• to teach formal methods for software specification.
• stresses the fundamental mathematical and engineering principles that should form the basis of software engineering.
• to integrate formal methods with software engineering practices.

Course Outcomes

At the end of the course the student should be able to

• demonstrate formal correctness of simple procedure.
• construct formal models of sequential software systems.
• implement sequential software systems based on formal models.
• verify attributes of formal models.
• describe the costs and benefits of formal methods.

Grading Policy

The tentative point distribution is as follows.

Homework Assignments	30%
Quiz	10%
Final exam	50%
Presentation	10%

Policies

• Late assignments will not be accepted unless an agreement is reached with the leturer.
• The class grades will be assigned using the Near East University's grading scale.
• Minimum attendance requirement is 70%.
• Cheating will not be tolerated.
• Attacks performed against University/Lecturer resources are expressly prohibited.

Textbook

• Flemming Nielson & Hanne Riis Nielson. Formal Methods An Appetizer. Springer. 2019
  Videos for the book are available at the YouTube channel FormalMethodsDK
  Slides for the book are available at the Google Drive
  FormalMethods.dk The learning environment for the book.

References

• F# Software Foundation
• Proof assistant
• List of tools for static code analysis
• List of model checking tools
• Bruce Mills, Practical Formal Software Engineering: Wanting the Software You Get, Cambridge University Press. 2019

Schedule

Week	Topic	Readings
1	Introduction	-
2 and 3	Program Graphs	Chapter 1
4 and 5	Guarded Commands Online lecture HW 1	Chapter 2
6 and 7	Program Verification Online lecture HW 1	Chapter 3
8 and 9	Program Analysis Online lecture HW 2	Chapter 5
10 and 11	Language-Based Security Online lecture	Chapter 6
12	Model Checking Online lecture	Chapter 7
13	Procedures Online lecture	Chapter 8
14	Concurrency Online lecture HW 3	Chapter 9
15	Review of the semester Online lecture	-
16	Final Exam: June 10, 10:00-12:00

The instructor reserves the right to make changes to the above syllabus as necessary. Students are responsible to be aware of changes announced in class and/or via the internet.