MK EN
ФИНКИ

Subject

Formal Methods

1. Course Title Formal Methods
Formal methods
2. Code KN-Z-03
3. Study Programme —
4. Organizer of the study programme (unit, institute, department or division) Faculty of Computer Science and Engineering
5. Degree level (first, second, third cycle) Second cycle
6. Academic year / semester 9 / Winter
7. Number of ECTS credits 6
8. Teacher Lasko Basnarkov, Vesna Dimitrievska Ristovska
9. Prerequisites for enrolling in the course —
10. Objectives of the course programme (competences) The course introduces students to the opportunities offered by formal methods, the categories of formal methods, and their use in building software architectures. It covers the complete methodology for the formal modelling, specification and verification of reactive systems. Upon completing the course, students are expected to understand the advantages that formal methods offer in computer engineering and to be able to model such systems in practice, as well as verify whether they satisfy their specifications.
11. Course content Fundamentals of formal methods. Modern techniques and tools for automated verification. Concurrent systems with a finite number of states. Model checking in concurrent finite-state systems. Modelling with transition systems. Modelling with temporal logic. Verification algorithms.
12. Learning methods NULL
13. Total available time 6 ECTS x 30 hours = 180 hours
14. Distribution of available time 60 + 30 + 0 + 60 + 30 = 180 hours
15. Forms of teaching activities
15.1. Lectures - theoretical instruction 60 hours
15.2. Exercises (laboratory, auditory), seminars, teamwork 30 hours
16. Other forms of activities
16.1. Project assignments 60 hours
16.2. Independent assignments 0 hours
16.3. Home study 30 hours
17. Assessment method
17.1. Tests 0 points
17.2. Seminar paper / project (presentation: written and oral) 60 points
17.3. Activities and learning 20 points
17.4. Final exam 0 points
18. Grading criteria (points / grade)
up to 50 points5 (five) (F)
from 51 to 60 points6 (six) (E)
from 61 to 70 points7 (seven) (D)
from 71 to 80 points8 (eight) (C)
from 81 to 90 points9 (nine) (B)
from 91 to 100 points10 (ten) (A)
19. Requirement for obtaining a signature and taking the final exam completed activities
20. Language of instruction NULL
21. Method for monitoring the quality of teaching NULL
22. Literature
22.1. Required literature
1. Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiři Srba | Reactive Systems: Modelling, Specification and Verification | Cambridge university press | 2007
2. C. A. R. Hoare | An Axiomatic Basis for Computer Programming | Communications of the ACM | 1969
3. C.J. Date | State - Based Model Checking of Event - Driven System Requirements | IEEE Transactions on Software Engineering | 2004
22.2. Additional literature
No. Author Title Publisher Year
Деканат Dean’s Office Студии Studies Акти Acts Проекти Projects